coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] overloading natural number notations for user types
- Date: Fri, 19 Feb 2016 22:59:02 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
- Ironport-phdr: 9a23:kupWIh9vAL2vBf9uRHKM819IXTAuvvDOBiVQ1KB91ukcTK2v8tzYMVDF4r011RmSDdqdtqoP0reM+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStGU0pz8jr3os7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGDGI7HERSHlesQBFCQLI9gqyCpL4sy/7sOV52TKGJuXsSro+VC6+7L1mQhXlkjxBMTpvozKfsdB5kK8O+EHpnBd42YOBOIw=
Hi Jonathan,
The parsers for numerals are implemented in OCaml. See for example plugins/syntax/nat_syntax.ml in the Coq source tree.
Best,
Robbert
On 02/19/2016 10:52 PM, Jonathan Leivent wrote:
Is there a way in Coq to overload the natural number notations? There
seems to be, because 42 in Z_scope is a Z, and 42 in bigZ_scope is a
BigZ.t_. However, in neither case is the Notation "42" itself defined.
At least in the case of bigZ_scope, the only notations defined are "0",
"1" and "2" (in Numbers/Integer/BigZ/BigZ.v) - and those are Local. So,
what magic makes it work for all other natural number notations as
well? And can it be used for user-defined types?
-- Jonathan
- [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/19/2016
- 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, 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.