Stream: Coq users

Topic: Notation introducing a binder

view this post on Zulip Gregory Malecha (Jul 01 2021 at 02:51):

It is possible to use a notation to introduce a binder that doesn't occur in the notation? e.g. something like:

Notation "'\this' X" := (fun this : ptr => X).

view this post on Zulip Clément Pit-Claudel (Jul 14 2021 at 05:58):

In Lisp land this is called an anaphoric macro, I asked about this a while back at . This is the best I'm aware of, and it's not great:

Class Arg1 {A} := { this: A }.
Notation "'\this' X" := (fun t => match {| this := t |} with _ => X end) (at level 100).

Check (\this this + 1).

Last updated: Oct 03 2023 at 21:01 UTC