max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix stdlib

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-16 21:59:44 -07:00
parent bb5a46cd61
commit 46e02bcdcc
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Prelude.lean
View file

@ -255,12 +255,12 @@ theorem decideEqFalse : [s : Decidable p] → Not p → Eq (decide p) false
| isFalse h, _ => rfl
theorem ofDecideEqTrue [s : Decidable p] : Eq (decide p) true → p := fun h =>
match s with
match (generalizing := false) s with
| isTrue h₁ => h₁
| isFalse h₁ => absurd h (neTrueOfEqFalse (decideEqFalse h₁))
theorem ofDecideEqFalse [s : Decidable p] : Eq (decide p) false → Not p := fun h =>
match s with
match (generalizing := false) s with
| isTrue h₁ => absurd h (neFalseOfEqTrue (decideEqTrue h₁))
| isFalse h₁ => h₁