Is it possible to get interpretation scopes to persist under lambdas? I have the following simple example:
Declare Scope foo_scope.
Notation "'BAR'" := 1%Z.
Notation "'BAR'" := 1%nat : foo_scope.
Delimit Scope foo_scope with foo.
Definition lalala {T : Type} (x : T) : T := x.
Arguments lalala {_} _%foo_scope.
(* BAR is interpreted according to foo_scope *)
Check lalala BAR.
(* = lalala 1 : nat *)
(* BAR is interpreted according to the global scope despite the fact that
the scope used to parse the argument is foo_scope... *)
Check lalala (fun x : unit => BAR).
(* = lalala (fun _ : unit => 1%Z) : unit -> Z *)
I know 0 ways to do literally that, but I declare lambdas with different scopes for the job, like in https://gitlab.mpi-sws.org/iris/iris/-/issues/320.
(** * 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.
see also https://github.com/coq/coq/issues/14305 https://github.com/coq/coq/pull/9123
The links reminded me the simple solution: make the function taking the lambda (above, lalala) into a notation that forces the scope.
Thanks @Gaëtan Gilbert ! That's exactly the functionality that I'm looking for with very nice semantics
Last updated: Oct 13 2024 at 01:02 UTC