michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(hott/init/datatypes): incorrect comment

Browse source
This commit is contained in:
ia0 2017-06-02 00:22:55 +02:00 committed by Floris van Doorn
parent 5ad4443237
commit cad1ed3395
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/init/datatypes.hlean
View file

@ -59,7 +59,7 @@ definition sigma.pr2 [reducible] [unfold 3] {A : Type} {B : A → Type} (p : sig
sigma.rec (λ a b, b) p
-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
-- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
-- The parser will generate the terms (pos (bit1 (bit0 (bit1 one)))), zero, and (pos (bit0 (bit1 (bit0 (bit1 one))))).
-- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
inductive pos_num : Type :=
| one : pos_num