summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar')
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst6
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst6
-rw-r--r--tests/fstar/misc/Loops.Funs.fst20
3 files changed, 16 insertions, 16 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 2074d02e..7137e92a 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -128,7 +128,7 @@ let rec hash_map_insert_in_list_loop_back
else
begin match hash_map_insert_in_list_loop_back t key value tl with
| Fail e -> Fail e
- | Return l -> Return (ListCons ckey cvalue l)
+ | Return tl0 -> Return (ListCons ckey cvalue tl0)
end
| ListNil -> let l = ListNil in Return (ListCons key value l)
end
@@ -413,7 +413,7 @@ let rec hash_map_get_mut_in_list_loop_back
else
begin match hash_map_get_mut_in_list_loop_back t tl key ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons ckey cvalue l)
+ | Return tl0 -> Return (ListCons ckey cvalue tl0)
end
| ListNil -> Fail Failure
end
@@ -514,7 +514,7 @@ let rec hash_map_remove_from_list_loop_back
else
begin match hash_map_remove_from_list_loop_back t key tl with
| Fail e -> Fail e
- | Return l -> Return (ListCons ckey x l)
+ | Return tl0 -> Return (ListCons ckey x tl0)
end
| ListNil -> Return ListNil
end
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index d2b87305..f3b480c3 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -137,7 +137,7 @@ let rec hashmap_hash_map_insert_in_list_loop_back
else
begin match hashmap_hash_map_insert_in_list_loop_back t key value tl with
| Fail e -> Fail e
- | Return l -> Return (HashmapListCons ckey cvalue l)
+ | Return tl0 -> Return (HashmapListCons ckey cvalue tl0)
end
| HashmapListNil ->
let l = HashmapListNil in Return (HashmapListCons key value l)
@@ -442,7 +442,7 @@ let rec hashmap_hash_map_get_mut_in_list_loop_back
else
begin match hashmap_hash_map_get_mut_in_list_loop_back t tl key ret with
| Fail e -> Fail e
- | Return l -> Return (HashmapListCons ckey cvalue l)
+ | Return tl0 -> Return (HashmapListCons ckey cvalue tl0)
end
| HashmapListNil -> Fail Failure
end
@@ -553,7 +553,7 @@ let rec hashmap_hash_map_remove_from_list_loop_back
else
begin match hashmap_hash_map_remove_from_list_loop_back t key tl with
| Fail e -> Fail e
- | Return l -> Return (HashmapListCons ckey x l)
+ | Return tl0 -> Return (HashmapListCons ckey x tl0)
end
| HashmapListNil -> Return HashmapListNil
end
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 73539cf6..3e8425dd 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -140,7 +140,7 @@ let rec list_nth_mut_loop_loop_back
| Return i0 ->
begin match list_nth_mut_loop_loop_back t tl i0 ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons x l)
+ | Return tl0 -> Return (ListCons x tl0)
end
end
| ListNil -> Fail Failure
@@ -201,7 +201,7 @@ let rec get_elem_mut_loop_back
else
begin match get_elem_mut_loop_back x tl ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons y l)
+ | Return tl0 -> Return (ListCons y tl0)
end
| ListNil -> Fail Failure
end
@@ -290,7 +290,7 @@ let rec list_nth_mut_loop_with_id_loop_back
| Return i0 ->
begin match list_nth_mut_loop_with_id_loop_back t i0 tl ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons x l)
+ | Return tl0 -> Return (ListCons x tl0)
end
end
| ListNil -> Fail Failure
@@ -379,7 +379,7 @@ let rec list_nth_mut_loop_pair_loop_back'a
| Return i0 ->
begin match list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons x0 l)
+ | Return tl00 -> Return (ListCons x0 tl00)
end
end
| ListNil -> Fail Failure
@@ -412,7 +412,7 @@ let rec list_nth_mut_loop_pair_loop_back'b
| Return i0 ->
begin match list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons x1 l)
+ | Return tl10 -> Return (ListCons x1 tl10)
end
end
| ListNil -> Fail Failure
@@ -500,7 +500,7 @@ let rec list_nth_mut_loop_pair_merge_loop_back
begin match list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret
with
| Fail e -> Fail e
- | Return (l, l0) -> Return (ListCons x0 l, ListCons x1 l0)
+ | Return (tl00, tl10) -> Return (ListCons x0 tl00, ListCons x1 tl10)
end
end
| ListNil -> Fail Failure
@@ -588,7 +588,7 @@ let rec list_nth_mut_shared_loop_pair_loop_back
begin match list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret
with
| Fail e -> Fail e
- | Return l -> Return (ListCons x0 l)
+ | Return tl00 -> Return (ListCons x0 tl00)
end
end
| ListNil -> Fail Failure
@@ -650,7 +650,7 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back
begin match
list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons x0 l)
+ | Return tl00 -> Return (ListCons x0 tl00)
end
end
| ListNil -> Fail Failure
@@ -711,7 +711,7 @@ let rec list_nth_shared_mut_loop_pair_loop_back
begin match list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret
with
| Fail e -> Fail e
- | Return l -> Return (ListCons x1 l)
+ | Return tl10 -> Return (ListCons x1 tl10)
end
end
| ListNil -> Fail Failure
@@ -773,7 +773,7 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back
begin match
list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons x1 l)
+ | Return tl10 -> Return (ListCons x1 tl10)
end
end
| ListNil -> Fail Failure
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 09:20:25 +0000