coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Where is notation for numbers ( 2=S (S O) )defined?
Date: Mon, 11 Nov 2013 23:02:19 +0100

On 11/11/2013 10:59 AM, Soegtrop, Michael wrote:

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?

It's being implemented by a plug in written in OCaml, see

plugins/syntax/nat_syntax.ml

in the Coq source tree.

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

I think coqide -nois is what you are looking for.

[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