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

chore: remove def implies

Browse source
This commit is contained in:
Mario Carneiro 2022-08-28 09:54:27 -04:00 • committed by Leonardo de Moura
parent cd0dd4cc2f
commit d4c7d0f266
1 changed files with 0 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/Core.lean
View file

@ -208,11 +208,6 @@ instance : LawfulBEq String := inferInstance
/-! # Logical connectives and equality -/
def implies (a b : Prop) := a → b
theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
fun hp => h₂ (h₁ hp)
def trivial : True := ⟨⟩
theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a :=