feat(logic/basic): is_trans Prop iff instance (#6836)

If you've ever wondered why `trans h1 h2` works for `≤` but not for `↔`, this is the reason.
leanprover-community · Mar 24, 2021 · 94a4a95 · 94a4a95
1 parent a008609
commit 94a4a95
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/logic/basic.lean b/src/logic/basic.lean
@@ -191,6 +191,9 @@ variables {a b c d : Prop}
 
 /-! ### Declarations about `implies` -/
 
+instance : is_refl Prop iff := ⟨iff.refl⟩
+instance : is_trans Prop iff := ⟨λ _ _ _, iff.trans⟩
+
 theorem iff_of_eq (e : a = b) : a ↔ b := e ▸ iff.rfl
 
 theorem iff_iff_eq : (a ↔ b) ↔ a = b := ⟨propext, iff_of_eq⟩