From fb9a1e93c2163b170979523f9a0cae90b472a16c Mon Sep 17 00:00:00 2001 From: Raito Bezarius Date: Wed, 17 Apr 2024 16:50:16 +0200 Subject: feat: factor everything in `OrdSpecRel` Now, we speak only about equivalence. Signed-off-by: Raito Bezarius --- AvlVerification/Specifications.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'AvlVerification/Specifications.lean') diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean index 0694df3..ac2d056 100644 --- a/AvlVerification/Specifications.lean +++ b/AvlVerification/Specifications.lean @@ -53,14 +53,10 @@ class OrdSpecInfaillible where class OrdSpecDuality extends OrdSpecInfaillible H where duality: ∀ a b, H.cmp a b = .ok .Greater -> H.cmp b a = .ok .Less --- TODO: OrdSpecEq := OrdSpecRel (R := Eq). -class OrdSpecEq extends OrdSpecInfaillible H where - equality: ∀ a b, H.cmp a b = .ok .Equal -> a = b - class OrdSpecRel (R: outParam (T -> T -> Prop)) extends OrdSpecInfaillible H where equivalence: ∀ a b, H.cmp a b = .ok .Equal -> R a b -class OrdSpecDualityEq extends OrdSpecDuality H, OrdSpecEq H +class OrdSpecDualityEq extends OrdSpecDuality H, OrdSpecRel H Eq instance: Coe (avl_verification.Ordering) (_root_.Ordering) where coe a := a.toLeanOrdering -- cgit v1.2.3