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

refactor(library/init): move num->nat coercion to init

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-01 08:23:31 -08:00
parent 193fed7061
commit b094c1cf43
2 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/data/nat/basic.lean
View file

@ -10,10 +10,6 @@ open eq.ops binary
namespace nat namespace nat
definition of_num [coercion] [reducible] (n : num) : ℕ :=
num.rec zero
(λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
definition addl (x y : ℕ) : ℕ := definition addl (x y : ℕ) : ℕ :=
nat.rec y (λ n r, succ r) x nat.rec y (λ n r, succ r) x
infix `⊕`:65 := addl infix `⊕`:65 := addl

3
library/init/nat.lean
View file

@ -338,4 +338,7 @@ namespace nat
(le.refl a) (le.refl a)
(λ b₁ ih, le.trans !pred_le ih) (λ b₁ ih, le.trans !pred_le ih)
definition of_num [coercion] [reducible] (n : num) : ℕ :=
num.rec zero
(λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
end nat end nat