diff options
author | Raito Bezarius | 2024-04-17 15:08:07 +0200 |
---|---|---|
committer | Raito Bezarius | 2024-04-17 15:08:07 +0200 |
commit | 945c630ec18e282bd0db731fb3f0b521e99de059 (patch) | |
tree | 5eefbf30b7a41612d61a5fe26223a59398af4fa2 /AvlVerification.lean | |
parent | 117cd1c0afbc50ffc5a90473cb4c01185188711e (diff) |
feat: add functional correctness of elements contained in the resulting tree
We revamp the typeclass mechanisms and we add an equality hypothesis
now.
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
Diffstat (limited to '')
-rw-r--r-- | AvlVerification.lean | 20 |
1 files changed, 6 insertions, 14 deletions
diff --git a/AvlVerification.lean b/AvlVerification.lean index b90680c..f9e6830 100644 --- a/AvlVerification.lean +++ b/AvlVerification.lean @@ -32,16 +32,8 @@ structure AVLTreeSet (T : Type) where def AVLTreeSet.new (T : Type) (OrdInst : Ord T) : Result (AVLTreeSet T) := Result.ok { root := none } -/- [avl_verification::{avl_verification::AVLTreeSet<T>}::find]: - Source: 'src/main.rs', lines 30:4-30:39 -/ -def AVLTreeSet.find - (T : Type) (OrdInst : Ord T) (self : AVLTreeSet T) (value : T) : - Result Bool - := - sorry - /- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]: loop 0: - Source: 'src/main.rs', lines 63:4-81:5 -/ + Source: 'src/main.rs', lines 43:4-61:5 -/ divergent def AVLTreeSet.insert_loop (T : Type) (OrdInst : Ord T) (value : T) (current_tree : Option (AVLNode T)) : @@ -69,17 +61,17 @@ divergent def AVLTreeSet.insert_loop Result.ok (b, some (AVLNode.mk t current_tree3 current_tree2)) /- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]: - Source: 'src/main.rs', lines 63:4-63:46 -/ + Source: 'src/main.rs', lines 43:4-43:46 -/ def AVLTreeSet.insert (T : Type) (OrdInst : Ord T) (self : AVLTreeSet T) (value : T) : Result (Bool × (AVLTreeSet T)) := do - let (b, as) ← AVLTreeSet.insert_loop T OrdInst value self.root - Result.ok (b, { root := as }) + let (b, u) ← AVLTreeSet.insert_loop T OrdInst value self.root + Result.ok (b, { root := u }) /- [avl_verification::{(avl_verification::Ord for u32)#1}::cmp]: - Source: 'src/main.rs', lines 85:4-85:43 -/ + Source: 'src/main.rs', lines 65:4-65:43 -/ def OrdU32.cmp (self : U32) (other : U32) : Result Ordering := if self < other then Result.ok Ordering.Less @@ -89,7 +81,7 @@ def OrdU32.cmp (self : U32) (other : U32) : Result Ordering := else Result.ok Ordering.Greater /- Trait implementation: [avl_verification::{(avl_verification::Ord for u32)#1}] - Source: 'src/main.rs', lines 84:0-84:16 -/ + Source: 'src/main.rs', lines 64:0-64:16 -/ def OrdU32 : Ord U32 := { cmp := OrdU32.cmp } |