From d4c7d0f266601af2fc25568d10959ea89e0e61dd Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sun, 28 Aug 2022 09:54:27 -0400
Subject: [PATCH] chore: remove `def implies`

---
 src/Init/Core.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 55fb9ddbe6..b8e0bc5432 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -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 :=