coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] overloading natural number notations for user types
- Date: Sun, 21 Feb 2016 18:05:16 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f172.google.com
- Ironport-phdr: 9a23:TJkBlBxI/42ZwJvXCy+O+j09IxM/srCxBDY+r6Qd0e4fIJqq85mqBkHD//Il1AaPBtWEra8fwLOI7+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZnsnLnsp9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULYQWD8hKiU+4NDhnRjFVwqGoHUGBDY4iB1NVirM9xb8FrjrtTDh/r5/0TKdO8LsSqsvCByt6q5qTFnjjyJRZG1xy33elsEl1PETmxmmvREqm4M=
I was thinking something stupider: you pass in terms that are treated as constructors and required to have the appropriate type signature (a type "NAT", an "O : NAT", and an "S : NAT -> NAT" (hopefully the code can be parametric over how many universes NAT uses, and whether its polymorphic or not, etc), and then notations get translated to applications of S and O, and applications of S and O get translated back, and if S and O happen to unfold to other things, then unfolding them breaks the notation (which is not the end of the world).
Even better would be to generalize the nat_syntax_plugin to handle things like [trunc_index], i.e., things where the base case should be displayed as 1 or as -2, etc.
I do not think that we should have to trust Ltac code to get syntax for custom natural numbers.
On Sun, Feb 21, 2016 at 5:49 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:
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
- Re: [Coq-Club] overloading natural number notations for user types, (continued)
- Re: [Coq-Club] overloading natural number notations for user types, Robbert Krebbers, 02/19/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/20/2016
- Re: [Coq-Club] overloading natural number notations for user types, Pierre-Marie Pédrot, 02/20/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/20/2016
- Re: [Coq-Club] overloading natural number notations for user types, Clément Pit--Claudel, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Assia Mahboubi, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Beta Ziliani, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Beta Ziliani, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jason Gross, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Pierre-Marie Pédrot, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jason Gross, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jason Gross, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Gregory Malecha, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/24/2016
- [Coq-Club] why are Coercions restricted to names?, Jonathan Leivent, 02/24/2016
- Re: [Coq-Club] why are Coercions restricted to names?, Jason Gross, 02/24/2016
- Re: [Coq-Club] why are Coercions restricted to names?, Jonathan Leivent, 02/25/2016
- Re: [Coq-Club] overloading natural number notations for user types, Pierre-Marie Pédrot, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Pierre-Marie Pédrot, 02/20/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/20/2016
- Re: [Coq-Club] overloading natural number notations for user types, Robbert Krebbers, 02/19/2016
Archive powered by MHonArc 2.6.18.