diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean index 2b9c15cbe..1eab93f4d 100644 --- a/library/init/datatypes.lean +++ b/library/init/datatypes.lean @@ -73,10 +73,21 @@ one : pos_num, bit1 : pos_num → pos_num, bit0 : pos_num → pos_num +namespace pos_num + definition succ (a : pos_num) : pos_num := + rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n) +end pos_num + inductive num : Type := zero : num, pos : pos_num → num +namespace num + open pos_num + definition succ (a : num) : num := + rec_on a (pos one) (λp, pos (succ p)) +end num + inductive bool : Type := ff : bool, tt : bool diff --git a/library/init/num.lean b/library/init/num.lean index f8a5172f9..c20d55bc5 100644 --- a/library/init/num.lean +++ b/library/init/num.lean @@ -13,9 +13,6 @@ definition pos_num.is_inhabited [instance] : inhabited pos_num := inhabited.mk pos_num.one namespace pos_num - definition succ (a : pos_num) : pos_num := - rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n) - definition is_one (a : pos_num) : bool := rec_on a tt (λn r, ff) (λn r, ff) @@ -55,8 +52,6 @@ inhabited.mk num.zero namespace num open pos_num - definition succ (a : num) : num := - rec_on a (pos one) (λp, pos (succ p)) definition pred (a : num) : num := rec_on a zero (λp, cond (is_one p) zero (pos (pred p)))