diff options
| author | Raito Bezarius | 2024-04-17 16:50:16 +0200 |
|---|---|---|
| committer | Raito Bezarius | 2024-04-17 16:50:16 +0200 |
| commit | fb9a1e93c2163b170979523f9a0cae90b472a16c (patch) | |
| tree | 4eb596d939fa2e08e5bd1e0c4e62b35dff528dbe /AvlVerification/Insert.lean | |
| parent | 945c630ec18e282bd0db731fb3f0b521e99de059 (diff) | |
feat: factor everything in `OrdSpecRel`
Now, we speak only about equivalence.
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
Diffstat (limited to 'AvlVerification/Insert.lean')
| -rw-r--r-- | AvlVerification/Insert.lean | 2 |
1 files changed, 1 insertions, 1 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) |