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

refactor(library/data/nat): rename to_nat to of_num

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-01 17:52:33 -07:00
parent 716cd4d651
commit a978e30c81
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/int/basic.lean
View file

@ -209,7 +209,7 @@ _
irreducible int irreducible int
definition of_nat [coercion] [reducible] (n : ℕ) : ℤ := psub (pair n 0) definition of_nat [coercion] [reducible] (n : ℕ) : ℤ := psub (pair n 0)
definition of_num [coercion] [reducible] (n : num) : ℤ := of_nat (nat.to_nat n) definition of_num [coercion] [reducible] (n : num) : ℤ := of_nat (nat.of_num n)
theorem eq_zero_intro (n : ℕ) : psub (pair n n) = 0 := theorem eq_zero_intro (n : ℕ) : psub (pair n n) = 0 :=
have H : rel (pair n n) (pair 0 0), by simp, have H : rel (pair n n) (pair 0 0), by simp,

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

@ -47,7 +47,7 @@ definition add (x y : ℕ) : ℕ :=
nat.rec x (λ n r, succ r) y nat.rec x (λ n r, succ r) y
infixl `+` := add infixl `+` := add
definition to_nat [coercion] [reducible] (n : num) : ℕ := definition of_num [coercion] [reducible] (n : num) : ℕ :=
num.rec zero num.rec zero
(λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n