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

refactor(library/logic/prop): allow 'absurd' to generate Type

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-21 19:39:16 -08:00
parent 2e121182de
commit acf1c501ad
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/logic/prop.lean
View file

@ -37,8 +37,8 @@ theorem not_intro {a : Prop} (H : a → false) : ¬a := H
--rename to not.elim or neg.elim
theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false := H1 H2
theorem absurd {a b : Prop} (H1 : a) (H2 : ¬a) : b :=
false_elim (H2 H1)
definition absurd {a : Prop} {b : Type} (H1 : a) (H2 : ¬a) : b :=
false.rec b (H2 H1)
theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a :=
assume Hna : ¬a, absurd Ha Hna