`observe` vs `_observe`
Opened this issue · 0 comments
wkolowski commented
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?