Could anybody provide a concrete example of what goes wrong if this remark is ignored and _observe is used instead of observe?
To quote:
(** Note that when [_observe] appears unapplied in an expression,
it is implicitly wrapped in a function. However, there is no
way to distinguish whether such wrapping took place, so relying
on this behavior can lead to confusion.
We recommend to always use a primitive projection applied,
and wrap it in a function explicitly like the above to pass
around as a first-order function. *)
@palmskog already asked this on Zulip, but the example given there has to do with reduction, which I think is not that bad. Besides reduction behaviour, what other issues might arise? Extensionality problems, like having to prove _observe = fun x => _observe x? Problems with term matching in Ltac? Problems with typeclass resolution?
Could anybody provide a concrete example of what goes wrong if this remark is ignored and
_observeis used instead ofobserve?To quote:
@palmskog already asked this on Zulip, but the example given there has to do with reduction, which I think is not that bad. Besides reduction behaviour, what other issues might arise? Extensionality problems, like having to prove
_observe = fun x => _observe x? Problems with term matching in Ltac? Problems with typeclass resolution?