From 123ef6ab6784b4b99f726663e3f3737972556560 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 15 Jun 2017 15:24:00 -0400 Subject: [PATCH] fix(datatypes): further fix incorrect comment --- hott/init/datatypes.hlean | 5 ++--- hott/init/reserved_notation.hlean | 8 ++++++++ library/init/datatypes.lean | 5 ++--- library/init/reserved_notation.lean | 8 ++++++++ 4 files changed, 20 insertions(+), 6 deletions(-) diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean index 7c4072831..f543894c9 100644 --- a/hott/init/datatypes.hlean +++ b/hott/init/datatypes.hlean @@ -58,9 +58,8 @@ sigma.rec (λ a b, a) p definition sigma.pr2 [reducible] [unfold 3] {A : Type} {B : A → Type} (p : sigma B) : B (sigma.pr1 p) := 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 (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). +-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26 +-- in an [priority n] flag. inductive pos_num : Type := | one : pos_num | bit1 : pos_num → pos_num diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean index 14f79ca39..f46015f51 100644 --- a/hott/init/reserved_notation.hlean +++ b/hott/init/reserved_notation.hlean @@ -37,6 +37,14 @@ definition lt {A : Type} [s : has_lt A] : A → A → Type := ha definition ge [reducible] {A : Type} [s : has_le A] (a b : A) : Type := le b a definition gt [reducible] {A : Type} [s : has_lt A] (a b : A) : Type := lt b a + +/- + bit0 and bit1 are two auxiliary definition used when parsing numerals such as 13, 0, 26. + The parser will generate the terms (bit1 (bit0 (bit1 one))), zero, and + (bit0 (bit1 (bit0 (bit1 one)))). This works in any type with an addition, a zero and a one. + More specifically, there must be type class instances for the classes for has_add, has_zero and + has_one +-/ definition bit0 [reducible] {A : Type} [s : has_add A] (a : A) : A := add a a definition bit1 [reducible] {A : Type} [s₁ : has_one A] [s₂ : has_add A] (a : A) : A := add (bit0 a) one diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean index acd6e7526..010fb258c 100644 --- a/library/init/datatypes.lean +++ b/library/init/datatypes.lean @@ -80,9 +80,8 @@ or.inr Hb structure sigma {A : Type} (B : A → Type) := mk :: (pr1 : A) (pr2 : B pr1) --- 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)))). --- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc). +-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26 +-- in an [priority n] flag. inductive pos_num : Type := | one : pos_num | bit1 : pos_num → pos_num diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index 55cad3d40..9b8bf634c 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -37,6 +37,14 @@ definition lt {A : Type} [s : has_lt A] : A → A → Prop := has_lt.lt definition ge [reducible] {A : Type} [s : has_le A] (a b : A) : Prop := le b a definition gt [reducible] {A : Type} [s : has_lt A] (a b : A) : Prop := lt b a + +/- + bit0 and bit1 are two auxiliary definition used when parsing numerals such as 13, 0, 26. + The parser will generate the terms (bit1 (bit0 (bit1 one))), zero, and + (bit0 (bit1 (bit0 (bit1 one)))). This works in any type with an addition, a zero and a one. + More specifically, there must be type class instances for the classes for has_add, has_zero and + has_one +-/ definition bit0 {A : Type} [s : has_add A] (a : A) : A := add a a definition bit1 {A : Type} [s₁ : has_one A] [s₂ : has_add A] (a : A) : A := add (bit0 a) one