summaryrefslogtreecommitdiff
path: root/tests/hashmap
diff options
context:
space:
mode:
authorSon Ho2022-02-13 11:53:56 +0100
committerSon Ho2022-02-13 11:53:56 +0100
commited88189ebe94d0aee97049465a1cb76fa3f8fcf2 (patch)
treefa911400a22d78084293debb689f0c32a7093749 /tests/hashmap
parent5dfe012bc12635cff9b83bf8bb0cb17a33e3d78a (diff)
Make minor modifications
Diffstat (limited to '')
-rw-r--r--tests/hashmap/Hashmap.Properties.fst8
1 files changed, 4 insertions, 4 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index ce43fc7c..9833d420 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -2828,7 +2828,7 @@ let hash_map_get_fwd_lem #t self key =
(*** get_mut'fwd *)
-(**** get_mut_in_list *)
+(**** get_mut_in_list'fwd *)
val hash_map_get_mut_in_list_fwd_lem
(#t : Type0) (key : usize) (ls : list_t t) :
@@ -2857,7 +2857,7 @@ let rec hash_map_get_mut_in_list_fwd_lem #t key ls =
end
#pop-options
-(**** get_mut *)
+(**** get_mut'fwd *)
val hash_map_get_mut_fwd_lem
(#t : Type0) (self : hash_map_t_nes t) (key : usize) :
@@ -2893,7 +2893,7 @@ let hash_map_get_mut_fwd_lem #t self key =
(*** get_mut'back *)
-(**** get_mut_in_list *)
+(**** get_mut_in_list'back *)
val hash_map_get_mut_in_list_back_lem
(#t : Type0) (key : usize) (ls : list_t t) (ret : t) :
@@ -2923,7 +2923,7 @@ let rec hash_map_get_mut_in_list_back_lem #t key ls ret =
end
#pop-options
-(**** get_mut *)
+(**** get_mut'back *)
/// Refinement lemma
val hash_map_get_mut_back_lem_refin