λne should use %I for body — or add a variant using `%I`.
For unbundled functions, I've used for a while a lambda notation that places the body automatically in bi_scope
:
(** * Notation for functions in the Iris scope. *)
Notation "'λI' x .. y , t" := (fun x => .. (fun y => t%I) ..)
(at level 200, x binder, y binder, right associativity,
only parsing) : function_scope.
Similarly, needing both λne
and %I
is annoying, what about:
Notation "'λneI' x .. y , t" :=
(@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t)%I _) ..) _)
(at level 200, x binder, y binder, right associativity).
I'd even consider placing that annotation in λne
itself – algebra.ofe
could import bi.notation
; but many non-expansive functions aren't predicates :-).