Coq seems to accept the following notation, but I can't seem to actually use it:

```
Notation "'%{' body '}'" := (fun _1 _2 => body) (at level 0).
Check %{ _1 + _2 }. (* Error: The reference _1 was not found in the current environment. *)
```

Is there a way to make anaphoric (unhygienic) notations in Coq?

The best I've found is typeclasses, and it's not the prettiest:

```
Class Args2 {A B} := { _1: A; _2: B }.
Notation "'%{' body '}'" := (fun a b => match {| _1 := a; _2 := b |} with inst => body end).
Check %{ _1 + _2 }.
```

(It pollutes the global environment)

Last updated: Jun 18 2024 at 09:02 UTC