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

fix(*/init/nat): fix occurrences where both theorem and [unfold-c] were used

Browse source
This commit is contained in:
Floris van Doorn 2015-06-04 21:39:50 -04:00
parent 1b414d36e7
commit 0b9c8e14a4
2 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
hott/init/nat.hlean
View file

@ -73,16 +73,16 @@ namespace nat
theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
theorem succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
definition succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
by induction H;reflexivity;exact le.step v_0
theorem pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
definition pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
by induction H;reflexivity;cases b;exact v_0;exact le.step v_0
theorem le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
definition le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
pred_le_pred H
theorem le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m :=
definition le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m :=
by cases n;exact le.step H;exact succ_le_succ H
theorem not_succ_le_self {n : ℕ} : ¬succ n ≤ n :=

8
library/init/nat.lean
View file

@ -73,16 +73,16 @@ namespace nat
theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
theorem succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
theorem succ_le_succ {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
by induction H;reflexivity;exact le.step v_0
theorem pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
theorem pred_le_pred {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
by induction H;reflexivity;cases b;exact v_0;exact le.step v_0
theorem le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
theorem le_of_succ_le_succ {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
pred_le_pred H
theorem le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m :=
theorem le_succ_of_pred_le {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m :=
by cases n;exact le.step H;exact succ_le_succ H
theorem not_succ_le_self {n : ℕ} : ¬succ n ≤ n :=