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 https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Anaphoric.20macros.3F/near/226227382 . 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: Feb 01 2023 at 13:03 UTC