Stream: Coq users

Topic: Interpretation scope applying under a function


view this post on Zulip 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 *)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jul 01 2021 at 09:00):

see also https://github.com/coq/coq/issues/14305 https://github.com/coq/coq/pull/9123

view this post on Zulip 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.

view this post on Zulip 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: Feb 08 2023 at 22:03 UTC