From 795ccf6e2b75e77bd9e8433673bcb2f27a1f2675 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Aug 2021 08:50:51 -0700 Subject: [PATCH] chore: add `Trans` instances for tutorial --- src/Init/Data/Nat/Basic.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 6a8949da42..1eda5d32f5 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -196,6 +196,18 @@ protected theorem lt_of_lt_of_le {n m k : Nat} : n < m → m ≤ k → n < k := protected theorem lt_of_lt_of_eq {n m k : Nat} : n < m → m = k → n < k := fun h₁ h₂ => h₂ ▸ h₁ +instance : Trans (. < . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop) where + trans := Nat.lt_trans + +instance : Trans (. ≤ . : Nat → Nat → Prop) (. ≤ . : Nat → Nat → Prop) (. ≤ . : Nat → Nat → Prop) where + trans := Nat.le_trans + +instance : Trans (. < . : Nat → Nat → Prop) (. ≤ . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop) where + trans := Nat.lt_of_lt_of_le + +instance : Trans (. ≤ . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop) where + trans := Nat.lt_of_le_of_lt + protected theorem le_of_eq {n m : Nat} (p : n = m) : n ≤ m := p ▸ Nat.le_refl n