The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 21/02/2016 23:31, Jason Gross wrote:
> How hard would it be to set up the syntax plugins already in Coq so that
> they registered vernaculars such as [Declare NatSyntax for nat in
> nat_scope [O S].] and similarly for notations for negative numbers,
> ascii, strings, etc?

Not that difficult, I believe. Yet, we need to rely on a meta-language
to pattern-match over terms. Ltac would fit the bill, but I personally
find this use a little bit ugly.  The vernacular would probably look like:

Parameter myNat : Type.

Ltac reify_myNat n :=
match n with
(* insert a code producing a Z from a myNat here *)
end.

Declare Nat Syntax myNat reify_myNat.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature