coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Where is notation for numbers ( 2=S (S O) )defined?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Where is notation for numbers ( 2=S (S O) )defined?
Date: Mon, 11 Nov 2013 09:59:54 +0000
Accept-language: de-DE, en-US

Dear Coq users,

just for the fun of it I looked into theories/init. One thing I couldn’t find in there is the definition of the notation for natural numbers e.g. 2=S (S O). I wonder how this actually works and how one creates such notations or assigns them to a type like nat or Z or binary naturals? Is it possible to create a binary or hexadecimal notation for naturals or e.g. a notation for a floating point type or some sort of advanced notation?

Also is it possible to run Coq in CoqIde without loading prelude.v, e.g. for educational purposes?

Thanks & best regards,

Michael

[Coq-Club] Question about notations, Jason Gross, 11/10/2013
- Re: [Coq-Club] Question about notations, Perry E. Metzger, 11/10/2013
  - Re: [Coq-Club] Question about notations, Gabriel Scherer, 11/10/2013
- [Coq-Club] Where is notation for numbers ( 2=S (S O) )defined?, Soegtrop, Michael, 11/11/2013
  - Re: [Coq-Club] Where is notation for numbers ( 2=S (S O) )defined?, Robbert Krebbers, 11/11/2013