coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] About numeral notations

From: 김형선 <hskiowa AT kaist.ac.kr>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] About numeral notations
Date: Wed, 4 Jul 2012 14:49:30 +0900 (KST)

Dear coq-club,

I read in Ch.12 of the reference book that numeral notations are defined in OCaml level, not in the Coq level. That sounded very understandable to me.
I wonder in which file the numerical notations are coded for nat, positive, Z, R, and Q. (I could not find a separate i.e. non-Coq-level numeral notation for Q, though.)

HyungSun Kim

[Coq-Club] About numeral notations, 김형선, 07/04/2012
- Re: [Coq-Club] About numeral notations, Pierre Letouzey, 07/06/2012