## Stream: Coq users

### Topic: Interpretation scope applying under a function

#### Gregory Malecha (Jul 01 2021 at 02:40):

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 *)
``````

#### Paolo Giarrusso (Jul 01 2021 at 05:58):

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.

#### Paolo Giarrusso (Jul 01 2021 at 05:59):

``````(** * 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.
``````

#### Paolo Giarrusso (Jul 01 2021 at 10:30):

The links reminded me the simple solution: make the function taking the lambda (above, lalala) into a notation that forces the scope.

#### Gregory Malecha (Jul 01 2021 at 11:52):

Thanks @Gaëtan Gilbert ! That's exactly the functionality that I'm looking for with very nice semantics

Last updated: Jun 14 2024 at 18:01 UTC