diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/hashmap/Hashmap/Funs.lean | 69 | ||||
| -rw-r--r-- | tests/lean/hashmap/Hashmap/Types.lean | 4 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 102 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Types.lean | 4 |
4 files changed, 83 insertions, 96 deletions
diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean index 0d83b04d..535ac9b2 100644 --- a/tests/lean/hashmap/Hashmap/Funs.lean +++ b/tests/lean/hashmap/Hashmap/Funs.lean @@ -16,7 +16,7 @@ def hash_map_allocate_slots_loop_fwd if h: n > (USize.ofNatCore 0 (by intlit)) then do - let slots0 ← vec_push_back (list_t T) slots list_t.ListNil + let slots0 ← vec_push_back (list_t T) slots list_t.Nil let n0 ← USize.checked_sub n (USize.ofNatCore 1 (by intlit)) hash_map_allocate_slots_loop_fwd T slots0 n0 else Result.ret slots @@ -63,7 +63,7 @@ def hash_map_clear_loop_fwd_back then do let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit)) - let slots0 ← vec_index_mut_back (list_t T) slots i list_t.ListNil + let slots0 ← vec_index_mut_back (list_t T) slots i list_t.Nil hash_map_clear_loop_fwd_back T slots0 i1 else Result.ret slots termination_by hash_map_clear_loop_fwd_back slots i => @@ -93,11 +93,11 @@ def hash_map_len_fwd (T : Type) (self : hash_map_t T) : Result USize := def hash_map_insert_in_list_loop_fwd (T : Type) (key : USize) (value : T) (ls : list_t T) : (Result Bool) := match h: ls with - | list_t.ListCons ckey cvalue tl => + | list_t.Cons ckey cvalue tl => if h: ckey = key then Result.ret false else hash_map_insert_in_list_loop_fwd T key value tl - | list_t.ListNil => Result.ret true + | list_t.Nil => Result.ret true termination_by hash_map_insert_in_list_loop_fwd key value ls => hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hash_map_insert_in_list_loop_decreases key value ls @@ -111,16 +111,15 @@ def hash_map_insert_in_list_fwd def hash_map_insert_in_list_loop_back (T : Type) (key : USize) (value : T) (ls : list_t T) : (Result (list_t T)) := match h: ls with - | list_t.ListCons ckey cvalue tl => + | list_t.Cons ckey cvalue tl => if h: ckey = key - then Result.ret (list_t.ListCons ckey value tl) + then Result.ret (list_t.Cons ckey value tl) else do let tl0 ← hash_map_insert_in_list_loop_back T key value tl - Result.ret (list_t.ListCons ckey cvalue tl0) - | list_t.ListNil => - let l := list_t.ListNil - Result.ret (list_t.ListCons key value l) + Result.ret (list_t.Cons ckey cvalue tl0) + | list_t.Nil => let l := list_t.Nil + Result.ret (list_t.Cons key value l) termination_by hash_map_insert_in_list_loop_back key value ls => hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hash_map_insert_in_list_loop_decreases key value ls @@ -167,11 +166,11 @@ def hash_map_move_elements_from_list_loop_fwd_back (Result (hash_map_t T)) := match h: ls with - | list_t.ListCons k v tl => + | list_t.Cons k v tl => do let ntable0 ← hash_map_insert_no_resize_fwd_back T ntable k v hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl - | list_t.ListNil => Result.ret ntable + | list_t.Nil => Result.ret ntable termination_by hash_map_move_elements_from_list_loop_fwd_back ntable ls => hash_map_move_elements_from_list_loop_terminates T ntable ls decreasing_by hash_map_move_elements_from_list_loop_decreases ntable ls @@ -191,10 +190,10 @@ def hash_map_move_elements_loop_fwd_back then do let l ← vec_index_mut_fwd (list_t T) slots i - let ls := mem_replace_fwd (list_t T) l list_t.ListNil + let ls := mem_replace_fwd (list_t T) l list_t.Nil let ntable0 ← hash_map_move_elements_from_list_fwd_back T ntable ls let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit)) - let l0 := mem_replace_back (list_t T) l list_t.ListNil + let l0 := mem_replace_back (list_t T) l list_t.Nil let slots0 ← vec_index_mut_back (list_t T) slots i l0 hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 else Result.ret (ntable, slots) @@ -251,11 +250,11 @@ def hash_map_insert_fwd_back def hash_map_contains_key_in_list_loop_fwd (T : Type) (key : USize) (ls : list_t T) : (Result Bool) := match h: ls with - | list_t.ListCons ckey t tl => + | list_t.Cons ckey t tl => if h: ckey = key then Result.ret true else hash_map_contains_key_in_list_loop_fwd T key tl - | list_t.ListNil => Result.ret false + | list_t.Nil => Result.ret false termination_by hash_map_contains_key_in_list_loop_fwd key ls => hash_map_contains_key_in_list_loop_terminates T key ls decreasing_by hash_map_contains_key_in_list_loop_decreases key ls @@ -279,11 +278,11 @@ def hash_map_contains_key_fwd def hash_map_get_in_list_loop_fwd (T : Type) (key : USize) (ls : list_t T) : (Result T) := match h: ls with - | list_t.ListCons ckey cvalue tl => + | list_t.Cons ckey cvalue tl => if h: ckey = key then Result.ret cvalue else hash_map_get_in_list_loop_fwd T key tl - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by hash_map_get_in_list_loop_fwd key ls => hash_map_get_in_list_loop_terminates T key ls decreasing_by hash_map_get_in_list_loop_decreases key ls @@ -307,11 +306,11 @@ def hash_map_get_fwd def hash_map_get_mut_in_list_loop_fwd (T : Type) (ls : list_t T) (key : USize) : (Result T) := match h: ls with - | list_t.ListCons ckey cvalue tl => + | list_t.Cons ckey cvalue tl => if h: ckey = key then Result.ret cvalue else hash_map_get_mut_in_list_loop_fwd T tl key - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by hash_map_get_mut_in_list_loop_fwd ls key => hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hash_map_get_mut_in_list_loop_decreases ls key @@ -325,14 +324,14 @@ def hash_map_get_mut_in_list_fwd def hash_map_get_mut_in_list_loop_back (T : Type) (ls : list_t T) (key : USize) (ret0 : T) : (Result (list_t T)) := match h: ls with - | list_t.ListCons ckey cvalue tl => + | list_t.Cons ckey cvalue tl => if h: ckey = key - then Result.ret (list_t.ListCons ckey ret0 tl) + then Result.ret (list_t.Cons ckey ret0 tl) else do let tl0 ← hash_map_get_mut_in_list_loop_back T tl key ret0 - Result.ret (list_t.ListCons ckey cvalue tl0) - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons ckey cvalue tl0) + | list_t.Nil => Result.fail Error.panic termination_by hash_map_get_mut_in_list_loop_back ls key ret0 => hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hash_map_get_mut_in_list_loop_decreases ls key @@ -370,16 +369,16 @@ def hash_map_get_mut_back def hash_map_remove_from_list_loop_fwd (T : Type) (key : USize) (ls : list_t T) : (Result (Option T)) := match h: ls with - | list_t.ListCons ckey t tl => + | list_t.Cons ckey t tl => if h: ckey = key then let mv_ls := - mem_replace_fwd (list_t T) (list_t.ListCons ckey t tl) list_t.ListNil + mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil match h: mv_ls with - | list_t.ListCons i cvalue tl0 => Result.ret (Option.some cvalue) - | list_t.ListNil => Result.fail Error.panic + | list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) + | list_t.Nil => Result.fail Error.panic else hash_map_remove_from_list_loop_fwd T key tl - | list_t.ListNil => Result.ret Option.none + | list_t.Nil => Result.ret Option.none termination_by hash_map_remove_from_list_loop_fwd key ls => hash_map_remove_from_list_loop_terminates T key ls decreasing_by hash_map_remove_from_list_loop_decreases key ls @@ -393,19 +392,19 @@ def hash_map_remove_from_list_fwd def hash_map_remove_from_list_loop_back (T : Type) (key : USize) (ls : list_t T) : (Result (list_t T)) := match h: ls with - | list_t.ListCons ckey t tl => + | list_t.Cons ckey t tl => if h: ckey = key then let mv_ls := - mem_replace_fwd (list_t T) (list_t.ListCons ckey t tl) list_t.ListNil + mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil match h: mv_ls with - | list_t.ListCons i cvalue tl0 => Result.ret tl0 - | list_t.ListNil => Result.fail Error.panic + | list_t.Cons i cvalue tl0 => Result.ret tl0 + | list_t.Nil => Result.fail Error.panic else do let tl0 ← hash_map_remove_from_list_loop_back T key tl - Result.ret (list_t.ListCons ckey t tl0) - | list_t.ListNil => Result.ret list_t.ListNil + Result.ret (list_t.Cons ckey t tl0) + | list_t.Nil => Result.ret list_t.Nil termination_by hash_map_remove_from_list_loop_back key ls => hash_map_remove_from_list_loop_terminates T key ls decreasing_by hash_map_remove_from_list_loop_decreases key ls diff --git a/tests/lean/hashmap/Hashmap/Types.lean b/tests/lean/hashmap/Hashmap/Types.lean index dd2be633..9e9e5c03 100644 --- a/tests/lean/hashmap/Hashmap/Types.lean +++ b/tests/lean/hashmap/Hashmap/Types.lean @@ -4,8 +4,8 @@ import Base.Primitives /- [hashmap::List] -/ inductive list_t (T : Type) := -| ListCons : USize -> T -> list_t T -> list_t T -| ListNil : list_t T +| Cons : USize -> T -> list_t T -> list_t T +| Nil : list_t T /- [hashmap::HashMap] -/ structure hash_map_t (T : Type) where diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index bf3a30e9..2be03d98 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -19,8 +19,7 @@ def hashmap_hash_map_allocate_slots_loop_fwd if h: n > (USize.ofNatCore 0 (by intlit)) then do - let slots0 ← - vec_push_back (hashmap_list_t T) slots hashmap_list_t.HashmapListNil + let slots0 ← vec_push_back (hashmap_list_t T) slots hashmap_list_t.Nil let n0 ← USize.checked_sub n (USize.ofNatCore 1 (by intlit)) hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 else Result.ret slots @@ -60,8 +59,8 @@ def hashmap_hash_map_new_fwd (T : Type) : Result (hashmap_hash_map_t T) := hashmap_hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by intlit)) (USize.ofNatCore 4 (by intlit)) (USize.ofNatCore 5 (by intlit)) -/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ -def hashmap_hash_map_clear_slots_loop_fwd_back +/- [hashmap_main::hashmap::HashMap::{0}::clear] -/ +def hashmap_hash_map_clear_loop_fwd_back (T : Type) (slots : Vec (hashmap_list_t T)) (i : USize) : (Result (Vec (hashmap_list_t T))) := @@ -71,28 +70,20 @@ def hashmap_hash_map_clear_slots_loop_fwd_back do let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit)) let slots0 ← - vec_index_mut_back (hashmap_list_t T) slots i - hashmap_list_t.HashmapListNil - hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1 + vec_index_mut_back (hashmap_list_t T) slots i hashmap_list_t.Nil + hashmap_hash_map_clear_loop_fwd_back T slots0 i1 else Result.ret slots -termination_by hashmap_hash_map_clear_slots_loop_fwd_back slots i => - hashmap_hash_map_clear_slots_loop_terminates T slots i -decreasing_by hashmap_hash_map_clear_slots_loop_decreases slots i - -/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ -def hashmap_hash_map_clear_slots_fwd_back - (T : Type) (slots : Vec (hashmap_list_t T)) : - Result (Vec (hashmap_list_t T)) - := - hashmap_hash_map_clear_slots_loop_fwd_back T slots - (USize.ofNatCore 0 (by intlit)) +termination_by hashmap_hash_map_clear_loop_fwd_back slots i => + hashmap_hash_map_clear_loop_terminates T slots i +decreasing_by hashmap_hash_map_clear_loop_decreases slots i /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ def hashmap_hash_map_clear_fwd_back (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := do let v ← - hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots + hashmap_hash_map_clear_loop_fwd_back T self.hashmap_hash_map_slots + (USize.ofNatCore 0 (by intlit)) Result.ret { self @@ -112,11 +103,11 @@ def hashmap_hash_map_insert_in_list_loop_fwd (Result Bool) := match h: ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => + | hashmap_list_t.Cons ckey cvalue tl => if h: ckey = key then Result.ret false else hashmap_hash_map_insert_in_list_loop_fwd T key value tl - | hashmap_list_t.HashmapListNil => Result.ret true + | hashmap_list_t.Nil => Result.ret true termination_by hashmap_hash_map_insert_in_list_loop_fwd key value ls => hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls @@ -132,16 +123,16 @@ def hashmap_hash_map_insert_in_list_loop_back (Result (hashmap_list_t T)) := match h: ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => + | hashmap_list_t.Cons ckey cvalue tl => if h: ckey = key - then Result.ret (hashmap_list_t.HashmapListCons ckey value tl) + then Result.ret (hashmap_list_t.Cons ckey value tl) else do let tl0 ← hashmap_hash_map_insert_in_list_loop_back T key value tl - Result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0) - | hashmap_list_t.HashmapListNil => - let l := hashmap_list_t.HashmapListNil - Result.ret (hashmap_list_t.HashmapListCons key value l) + Result.ret (hashmap_list_t.Cons ckey cvalue tl0) + | hashmap_list_t.Nil => + let l := hashmap_list_t.Nil + Result.ret (hashmap_list_t.Cons key value l) termination_by hashmap_hash_map_insert_in_list_loop_back key value ls => hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls @@ -199,11 +190,11 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back (Result (hashmap_hash_map_t T)) := match h: ls with - | hashmap_list_t.HashmapListCons k v tl => + | hashmap_list_t.Cons k v tl => do let ntable0 ← hashmap_hash_map_insert_no_resize_fwd_back T ntable k v hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl - | hashmap_list_t.HashmapListNil => Result.ret ntable + | hashmap_list_t.Nil => Result.ret ntable termination_by hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls => hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls @@ -227,13 +218,11 @@ def hashmap_hash_map_move_elements_loop_fwd_back then do let l ← vec_index_mut_fwd (hashmap_list_t T) slots i - let ls := - mem_replace_fwd (hashmap_list_t T) l hashmap_list_t.HashmapListNil + let ls := mem_replace_fwd (hashmap_list_t T) l hashmap_list_t.Nil let ntable0 ← hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit)) - let l0 := - mem_replace_back (hashmap_list_t T) l hashmap_list_t.HashmapListNil + let l0 := mem_replace_back (hashmap_list_t T) l hashmap_list_t.Nil let slots0 ← vec_index_mut_back (hashmap_list_t T) slots i l0 hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 else Result.ret (ntable, slots) @@ -291,11 +280,11 @@ def hashmap_hash_map_insert_fwd_back def hashmap_hash_map_contains_key_in_list_loop_fwd (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result Bool) := match h: ls with - | hashmap_list_t.HashmapListCons ckey t tl => + | hashmap_list_t.Cons ckey t tl => if h: ckey = key then Result.ret true else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl - | hashmap_list_t.HashmapListNil => Result.ret false + | hashmap_list_t.Nil => Result.ret false termination_by hashmap_hash_map_contains_key_in_list_loop_fwd key ls => hashmap_hash_map_contains_key_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_contains_key_in_list_loop_decreases key ls @@ -320,11 +309,11 @@ def hashmap_hash_map_contains_key_fwd def hashmap_hash_map_get_in_list_loop_fwd (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result T) := match h: ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => + | hashmap_list_t.Cons ckey cvalue tl => if h: ckey = key then Result.ret cvalue else hashmap_hash_map_get_in_list_loop_fwd T key tl - | hashmap_list_t.HashmapListNil => Result.fail Error.panic + | hashmap_list_t.Nil => Result.fail Error.panic termination_by hashmap_hash_map_get_in_list_loop_fwd key ls => hashmap_hash_map_get_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls @@ -349,11 +338,11 @@ def hashmap_hash_map_get_fwd def hashmap_hash_map_get_mut_in_list_loop_fwd (T : Type) (ls : hashmap_list_t T) (key : USize) : (Result T) := match h: ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => + | hashmap_list_t.Cons ckey cvalue tl => if h: ckey = key then Result.ret cvalue else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key - | hashmap_list_t.HashmapListNil => Result.fail Error.panic + | hashmap_list_t.Nil => Result.fail Error.panic termination_by hashmap_hash_map_get_mut_in_list_loop_fwd ls key => hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key @@ -369,14 +358,14 @@ def hashmap_hash_map_get_mut_in_list_loop_back (Result (hashmap_list_t T)) := match h: ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => + | hashmap_list_t.Cons ckey cvalue tl => if h: ckey = key - then Result.ret (hashmap_list_t.HashmapListCons ckey ret0 tl) + then Result.ret (hashmap_list_t.Cons ckey ret0 tl) else do let tl0 ← hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 - Result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0) - | hashmap_list_t.HashmapListNil => Result.fail Error.panic + Result.ret (hashmap_list_t.Cons ckey cvalue tl0) + | hashmap_list_t.Nil => Result.fail Error.panic termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 => hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key @@ -420,18 +409,17 @@ def hashmap_hash_map_get_mut_back def hashmap_hash_map_remove_from_list_loop_fwd (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result (Option T)) := match h: ls with - | hashmap_list_t.HashmapListCons ckey t tl => + | hashmap_list_t.Cons ckey t tl => if h: ckey = key then let mv_ls := - mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons ckey - t tl) hashmap_list_t.HashmapListNil + mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl) + hashmap_list_t.Nil match h: mv_ls with - | hashmap_list_t.HashmapListCons i cvalue tl0 => - Result.ret (Option.some cvalue) - | hashmap_list_t.HashmapListNil => Result.fail Error.panic + | hashmap_list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) + | hashmap_list_t.Nil => Result.fail Error.panic else hashmap_hash_map_remove_from_list_loop_fwd T key tl - | hashmap_list_t.HashmapListNil => Result.ret Option.none + | hashmap_list_t.Nil => Result.ret Option.none termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls => hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls @@ -447,20 +435,20 @@ def hashmap_hash_map_remove_from_list_loop_back (Result (hashmap_list_t T)) := match h: ls with - | hashmap_list_t.HashmapListCons ckey t tl => + | hashmap_list_t.Cons ckey t tl => if h: ckey = key then let mv_ls := - mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons ckey - t tl) hashmap_list_t.HashmapListNil + mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl) + hashmap_list_t.Nil match h: mv_ls with - | hashmap_list_t.HashmapListCons i cvalue tl0 => Result.ret tl0 - | hashmap_list_t.HashmapListNil => Result.fail Error.panic + | hashmap_list_t.Cons i cvalue tl0 => Result.ret tl0 + | hashmap_list_t.Nil => Result.fail Error.panic else do let tl0 ← hashmap_hash_map_remove_from_list_loop_back T key tl - Result.ret (hashmap_list_t.HashmapListCons ckey t tl0) - | hashmap_list_t.HashmapListNil => Result.ret hashmap_list_t.HashmapListNil + Result.ret (hashmap_list_t.Cons ckey t tl0) + | hashmap_list_t.Nil => Result.ret hashmap_list_t.Nil termination_by hashmap_hash_map_remove_from_list_loop_back key ls => hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean index fbab1bcd..989dd2a9 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean @@ -4,8 +4,8 @@ import Base.Primitives /- [hashmap_main::hashmap::List] -/ inductive hashmap_list_t (T : Type) := -| HashmapListCons : USize -> T -> hashmap_list_t T -> hashmap_list_t T -| HashmapListNil : hashmap_list_t T +| Cons : USize -> T -> hashmap_list_t T -> hashmap_list_t T +| Nil : hashmap_list_t T /- [hashmap_main::hashmap::HashMap] -/ structure hashmap_hash_map_t (T : Type) where |