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

chore(builtin/Nat): use iff

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-16 02:06:53 -08:00
parent 4dc98bc73b
commit 398d83b6d5
2 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/builtin/Nat.lean
View file

@ -36,7 +36,7 @@ axiom add_zeror (a : Nat) : a + 0 = a
axiom add_succr (a b : Nat) : a + (b + 1) = (a + b) + 1 axiom add_succr (a b : Nat) : a + (b + 1) = (a + b) + 1
axiom mul_zeror (a : Nat) : a * 0 = 0 axiom mul_zeror (a : Nat) : a * 0 = 0
axiom mul_succr (a b : Nat) : a * (b + 1) = a * b + a axiom mul_succr (a b : Nat) : a * (b + 1) = a * b + a
axiom le_def (a b : Nat) : a ≤ b = ∃ c, a + c = b axiom le_def (a b : Nat) : a ≤ b ⟷ ∃ c, a + c = b
axiom induction {P : Nat → Bool} (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : ∀ a, P a axiom induction {P : Nat → Bool} (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : ∀ a, P a
theorem induction_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a theorem induction_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a

BIN
src/builtin/obj/Nat.olean
View file

Binary file not shown.