diff options
| -rw-r--r-- | AvlVerification/Insert.lean | 2 | ||||
| -rw-r--r-- | AvlVerification/Specifications.lean | 6 |
2 files changed, 2 insertions, 6 deletions
diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean index 16e740f..f5b7958 100644 --- a/AvlVerification/Insert.lean +++ b/AvlVerification/Insert.lean @@ -134,7 +134,7 @@ lemma AVLTreeSet.insert_loop_spec_global { simp; split_conjs . tauto - . simp [Ospec.equality _ _ Hordering] + . simp [Ospec.equivalence _ _ Hordering] } { have ⟨ added₂, left₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a left (BST.left Hbst) 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 |