Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] overloading natural number notations for user types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] overloading natural number notations for user types


Chronological Thread 
  • 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


Archive powered by MHonArc 2.6.18.

Top of Page