Stream: Coq users

Topic: Anaphoric macros?


view this post on Zulip 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?

view this post on Zulip 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: Feb 08 2023 at 23:03 UTC