Clément Pit-Claudel (Feb 13 2021 at 05:04): Clément Pit-Claudel (Feb 13 2021 at 05:04):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?
Clément Pit-Claudel (Feb 13 2021 at 05:11):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: Oct 13 2024 at 01:02 UTC