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

refactor(library/init): move num.succ to init.datatypes

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-05 10:29:06 -08:00
parent 5e228d92d2
commit 23fa16a23d
2 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
library/init/datatypes.lean
View file

@ -73,10 +73,21 @@ one : pos_num,
bit1 : pos_num → pos_num, bit1 : pos_num → pos_num,
bit0 : 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 := inductive num : Type :=
zero : num, zero : num,
pos : pos_num → 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 := inductive bool : Type :=
ff : bool, ff : bool,
tt : bool tt : bool

5
library/init/num.lean
View file

@ -13,9 +13,6 @@ definition pos_num.is_inhabited [instance] : inhabited pos_num :=
inhabited.mk pos_num.one inhabited.mk pos_num.one
namespace 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)
definition is_one (a : pos_num) : bool := definition is_one (a : pos_num) : bool :=
rec_on a tt (λn r, ff) (λn r, ff) rec_on a tt (λn r, ff) (λn r, ff)
@ -55,8 +52,6 @@ inhabited.mk num.zero
namespace num namespace num
open pos_num open pos_num
definition succ (a : num) : num :=
rec_on a (pos one) (λp, pos (succ p))
definition pred (a : num) : num := definition pred (a : num) : num :=
rec_on a zero (λp, cond (is_one p) zero (pos (pred p))) rec_on a zero (λp, cond (is_one p) zero (pos (pred p)))