From cad1ed33952be1307259f29febc72206665185fe Mon Sep 17 00:00:00 2001
From: ia0 <git@ia0.eu>
Date: Fri, 2 Jun 2017 00:22:55 +0200
Subject: [PATCH] fix(hott/init/datatypes): incorrect comment

---
 hott/init/datatypes.hlean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean
index 7e626f8ac..7c4072831 100644
--- a/hott/init/datatypes.hlean
+++ b/hott/init/datatypes.hlean
@@ -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