Gregory Malecha (Jul 01 2021 at 02:51): 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).
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: Oct 03 2023 at 21:01 UTC