summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v12
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v12
-rw-r--r--tests/coq/misc/Loops.v8
-rw-r--r--tests/fstar/hashmap/Hashmap.Clauses.Template.fst4
-rw-r--r--tests/fstar/hashmap/Hashmap.Clauses.fst4
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst16
-rw-r--r--tests/fstar/hashmap/Hashmap.Properties.fst28
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst4
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst4
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst16
-rw-r--r--tests/fstar/misc/Loops.Clauses.Template.fst2
-rw-r--r--tests/fstar/misc/Loops.Clauses.fst4
-rw-r--r--tests/fstar/misc/Loops.Funs.fst10
13 files changed, 62 insertions, 62 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 1cbff379..9c65fb46 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -332,7 +332,7 @@ Definition hash_map_get_fwd
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
Fixpoint hash_map_get_mut_in_list_loop_fwd
- (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
+ (T : Type) (n : nat) (ls : List_t T) (key : usize) : result T :=
match n with
| O => Fail_ OutOfFuel
| S n0 =>
@@ -340,7 +340,7 @@ Fixpoint hash_map_get_mut_in_list_loop_fwd
| ListCons ckey cvalue tl =>
if ckey s= key
then Return cvalue
- else hash_map_get_mut_in_list_loop_fwd T n0 key tl
+ else hash_map_get_mut_in_list_loop_fwd T n0 tl key
| ListNil => Fail_ Failure
end
end
@@ -349,12 +349,12 @@ Fixpoint hash_map_get_mut_in_list_loop_fwd
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
Definition hash_map_get_mut_in_list_fwd
(T : Type) (n : nat) (ls : List_t T) (key : usize) : result T :=
- hash_map_get_mut_in_list_loop_fwd T n key ls
+ hash_map_get_mut_in_list_loop_fwd T n ls key
.
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
Fixpoint hash_map_get_mut_in_list_loop_back
- (T : Type) (n : nat) (key : usize) (ls : List_t T) (ret : T) :
+ (T : Type) (n : nat) (ls : List_t T) (key : usize) (ret : T) :
result (List_t T)
:=
match n with
@@ -365,7 +365,7 @@ Fixpoint hash_map_get_mut_in_list_loop_back
if ckey s= key
then Return (ListCons ckey ret tl)
else (
- l <- hash_map_get_mut_in_list_loop_back T n0 key tl ret;
+ l <- hash_map_get_mut_in_list_loop_back T n0 tl key ret;
Return (ListCons ckey cvalue l))
| ListNil => Fail_ Failure
end
@@ -377,7 +377,7 @@ Definition hash_map_get_mut_in_list_back
(T : Type) (n : nat) (ls : List_t T) (key : usize) (ret : T) :
result (List_t T)
:=
- hash_map_get_mut_in_list_loop_back T n key ls ret
+ hash_map_get_mut_in_list_loop_back T n ls key ret
.
(** [hashmap::HashMap::{0}::get_mut] *)
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 2a8ab5b5..94a9e6a5 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -358,7 +358,7 @@ Definition hashmap_hash_map_get_fwd
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
- (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
+ (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T :=
match n with
| O => Fail_ OutOfFuel
| S n0 =>
@@ -366,7 +366,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
| HashmapListCons ckey cvalue tl =>
if ckey s= key
then Return cvalue
- else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 key tl
+ else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 tl key
| HashmapListNil => Fail_ Failure
end
end
@@ -375,12 +375,12 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
Definition hashmap_hash_map_get_mut_in_list_fwd
(T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T :=
- hashmap_hash_map_get_mut_in_list_loop_fwd T n key ls
+ hashmap_hash_map_get_mut_in_list_loop_fwd T n ls key
.
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
- (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) (ret : T) :
+ (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) :
result (Hashmap_list_t T)
:=
match n with
@@ -391,7 +391,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
if ckey s= key
then Return (HashmapListCons ckey ret tl)
else (
- l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 key tl ret;
+ l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 tl key ret;
Return (HashmapListCons ckey cvalue l))
| HashmapListNil => Fail_ Failure
end
@@ -403,7 +403,7 @@ Definition hashmap_hash_map_get_mut_in_list_back
(T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) :
result (Hashmap_list_t T)
:=
- hashmap_hash_map_get_mut_in_list_loop_back T n key ls ret
+ hashmap_hash_map_get_mut_in_list_loop_back T n ls key ret
.
(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 4fbb7da0..9d416bb0 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -235,16 +235,16 @@ Definition get_elem_mut_back
(** [loops::get_elem_shared] *)
Fixpoint get_elem_shared_loop_fwd
- (n : nat) (x : usize) (slots : vec (List_t usize)) (ls : List_t usize)
+ (n : nat) (slots : vec (List_t usize)) (x : usize) (ls : List_t usize)
(ls0 : List_t usize) :
result usize
:=
match n with
| O => Fail_ OutOfFuel
| S n0 =>
- match ls0 with
+ match ls with
| ListCons y tl =>
- if y s= x then Return y else get_elem_shared_loop_fwd n0 x slots ls tl
+ if y s= x then Return y else get_elem_shared_loop_fwd n0 slots x tl ls0
| ListNil => Fail_ Failure
end
end
@@ -254,7 +254,7 @@ Fixpoint get_elem_shared_loop_fwd
Definition get_elem_shared_fwd
(n : nat) (slots : vec (List_t usize)) (x : usize) : result usize :=
l <- vec_index_fwd (List_t usize) slots (0%usize);
- get_elem_shared_loop_fwd n x slots l l
+ get_elem_shared_loop_fwd n slots x l l
.
(** [loops::id_mut] *)
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
index 3e51c6f1..ce86071c 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
@@ -54,8 +54,8 @@ let hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) :
(** [hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *)
unfold
-let hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
- (ls : list_t t) : nat =
+let hash_map_get_mut_in_list_decreases (t : Type0) (ls : list_t t)
+ (key : usize) : nat =
admit ()
(** [hashmap::HashMap::{0}::remove_from_list]: decreases clause *)
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.fst b/tests/fstar/hashmap/Hashmap.Clauses.fst
index 4f3e37e9..2a9c0242 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.fst
@@ -49,8 +49,8 @@ let hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) :
(** [hashmap::HashMap::get_mut_in_list]: decreases clause *)
unfold
-let hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
- (ls : list_t t) : list_t t =
+let hash_map_get_mut_in_list_decreases (t : Type0) (ls : list_t t)
+ (key : usize) : list_t t =
ls
(** [hashmap::HashMap::remove_from_list]: decreases clause *)
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 81b253ad..14cea9cb 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -384,34 +384,34 @@ let hash_map_get_fwd
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
let rec hash_map_get_mut_in_list_loop_fwd
- (t : Type0) (key : usize) (ls : list_t t) :
- Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t key ls))
+ (t : Type0) (ls : list_t t) (key : usize) :
+ Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t ls key))
=
begin match ls with
| ListCons ckey cvalue tl ->
if ckey = key
then Return cvalue
- else hash_map_get_mut_in_list_loop_fwd t key tl
+ else hash_map_get_mut_in_list_loop_fwd t tl key
| ListNil -> Fail Failure
end
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
let hash_map_get_mut_in_list_fwd
(t : Type0) (ls : list_t t) (key : usize) : result t =
- hash_map_get_mut_in_list_loop_fwd t key ls
+ hash_map_get_mut_in_list_loop_fwd t ls key
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
let rec hash_map_get_mut_in_list_loop_back
- (t : Type0) (key : usize) (ls : list_t t) (ret : t) :
+ (t : Type0) (ls : list_t t) (key : usize) (ret : t) :
Tot (result (list_t t))
- (decreases (hash_map_get_mut_in_list_decreases t key ls))
+ (decreases (hash_map_get_mut_in_list_decreases t ls key))
=
begin match ls with
| ListCons ckey cvalue tl ->
if ckey = key
then Return (ListCons ckey ret tl)
else
- begin match hash_map_get_mut_in_list_loop_back t key tl ret with
+ 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)
end
@@ -421,7 +421,7 @@ let rec hash_map_get_mut_in_list_loop_back
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
let hash_map_get_mut_in_list_back
(t : Type0) (ls : list_t t) (key : usize) (ret : t) : result (list_t t) =
- hash_map_get_mut_in_list_loop_back t key ls ret
+ hash_map_get_mut_in_list_loop_back t ls key ret
(** [hashmap::HashMap::{0}::get_mut] *)
let hash_map_get_mut_fwd
diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index 724ca741..e1d0a541 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -2704,16 +2704,16 @@ let hash_map_get_fwd_lem #t self key = hash_map_get_fwd_lem_aux #t self key
(**** get_mut_in_list'fwd *)
val hash_map_get_mut_in_list_loop_fwd_lem
- (#t : Type0) (key : usize) (ls : list_t t) :
+ (#t : Type0) (ls : list_t t) (key : usize) :
Lemma
(ensures (
- match hash_map_get_mut_in_list_loop_fwd t key ls, slot_t_find_s key ls with
+ match hash_map_get_mut_in_list_loop_fwd t ls key, slot_t_find_s key ls with
| Fail _, None -> True
| Return x, Some x' -> x == x'
| _ -> False))
#push-options "--fuel 1"
-let rec hash_map_get_mut_in_list_loop_fwd_lem #t key ls =
+let rec hash_map_get_mut_in_list_loop_fwd_lem #t ls key =
begin match ls with
| ListCons ckey cvalue ls0 ->
let b = ckey = key in
@@ -2721,8 +2721,8 @@ let rec hash_map_get_mut_in_list_loop_fwd_lem #t key ls =
then ()
else
begin
- hash_map_get_mut_in_list_loop_fwd_lem key ls0;
- match hash_map_get_mut_in_list_loop_fwd t key ls0 with
+ hash_map_get_mut_in_list_loop_fwd_lem ls0 key;
+ match hash_map_get_mut_in_list_loop_fwd t ls0 key with
| Fail _ -> ()
| Return x -> ()
end
@@ -2754,8 +2754,8 @@ let hash_map_get_mut_fwd_lem_aux #t self key =
| Fail _ -> ()
| Return l ->
begin
- hash_map_get_mut_in_list_loop_fwd_lem key l;
- match hash_map_get_mut_in_list_loop_fwd t key l with
+ hash_map_get_mut_in_list_loop_fwd_lem l key;
+ match hash_map_get_mut_in_list_loop_fwd t l key with
| Fail _ -> ()
| Return x -> ()
end
@@ -2771,17 +2771,17 @@ let hash_map_get_mut_fwd_lem #t self key =
(**** get_mut_in_list'back *)
val hash_map_get_mut_in_list_loop_back_lem
- (#t : Type0) (key : usize) (ls : list_t t) (ret : t) :
+ (#t : Type0) (ls : list_t t) (key : usize) (ret : t) :
Lemma
(requires (Some? (slot_t_find_s key ls)))
(ensures (
- match hash_map_get_mut_in_list_loop_back t key ls ret with
+ match hash_map_get_mut_in_list_loop_back t ls key ret with
| Fail _ -> False
| Return ls' -> list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,ret)
| _ -> False))
#push-options "--fuel 1"
-let rec hash_map_get_mut_in_list_loop_back_lem #t key ls ret =
+let rec hash_map_get_mut_in_list_loop_back_lem #t ls key ret =
begin match ls with
| ListCons ckey cvalue ls0 ->
let b = ckey = key in
@@ -2789,8 +2789,8 @@ let rec hash_map_get_mut_in_list_loop_back_lem #t key ls ret =
then let ls1 = ListCons ckey ret ls0 in ()
else
begin
- hash_map_get_mut_in_list_loop_back_lem key ls0 ret;
- match hash_map_get_mut_in_list_loop_back t key ls0 ret with
+ hash_map_get_mut_in_list_loop_back_lem ls0 key ret;
+ match hash_map_get_mut_in_list_loop_back t ls0 key ret with
| Fail _ -> ()
| Return l -> let ls1 = ListCons ckey cvalue l in ()
end
@@ -2828,8 +2828,8 @@ let hash_map_get_mut_back_lem_refin #t self key ret =
| Fail _ -> ()
| Return l ->
begin
- hash_map_get_mut_in_list_loop_back_lem key l ret;
- match hash_map_get_mut_in_list_loop_back t key l ret with
+ hash_map_get_mut_in_list_loop_back_lem l key ret;
+ match hash_map_get_mut_in_list_loop_back t l key ret with
| Fail _ -> ()
| Return l0 ->
begin match vec_index_mut_back (list_t t) v hash_mod l0 with
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
index 55685114..871de28a 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
@@ -55,8 +55,8 @@ let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize)
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *)
unfold
-let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
- (ls : hashmap_list_t t) : nat =
+let hashmap_hash_map_get_mut_in_list_decreases (t : Type0)
+ (ls : hashmap_list_t t) (key : usize) : nat =
admit ()
(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: decreases clause *)
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
index b864e32a..8afe2523 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
@@ -49,8 +49,8 @@ let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : hashm
(** [hashmap::HashMap::get_mut_in_list]: decreases clause *)
unfold
-let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
- (ls : hashmap_list_t t) : hashmap_list_t t =
+let hashmap_hash_map_get_mut_in_list_decreases (t : Type0)
+ (ls : hashmap_list_t t) (key : usize) : hashmap_list_t t =
ls
(** [hashmap::HashMap::remove_from_list]: decreases clause *)
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index fdbf1404..42ee2a17 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -410,35 +410,35 @@ let hashmap_hash_map_get_fwd
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
let rec hashmap_hash_map_get_mut_in_list_loop_fwd
- (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+ (t : Type0) (ls : hashmap_list_t t) (key : usize) :
Tot (result t)
- (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls))
+ (decreases (hashmap_hash_map_get_mut_in_list_decreases t ls key))
=
begin match ls with
| HashmapListCons ckey cvalue tl ->
if ckey = key
then Return cvalue
- else hashmap_hash_map_get_mut_in_list_loop_fwd t key tl
+ else hashmap_hash_map_get_mut_in_list_loop_fwd t tl key
| HashmapListNil -> Fail Failure
end
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
let hashmap_hash_map_get_mut_in_list_fwd
(t : Type0) (ls : hashmap_list_t t) (key : usize) : result t =
- hashmap_hash_map_get_mut_in_list_loop_fwd t key ls
+ hashmap_hash_map_get_mut_in_list_loop_fwd t ls key
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
let rec hashmap_hash_map_get_mut_in_list_loop_back
- (t : Type0) (key : usize) (ls : hashmap_list_t t) (ret : t) :
+ (t : Type0) (ls : hashmap_list_t t) (key : usize) (ret : t) :
Tot (result (hashmap_list_t t))
- (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls))
+ (decreases (hashmap_hash_map_get_mut_in_list_decreases t ls key))
=
begin match ls with
| HashmapListCons ckey cvalue tl ->
if ckey = key
then Return (HashmapListCons ckey ret tl)
else
- begin match hashmap_hash_map_get_mut_in_list_loop_back t key tl ret with
+ 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)
end
@@ -450,7 +450,7 @@ let hashmap_hash_map_get_mut_in_list_back
(t : Type0) (ls : hashmap_list_t t) (key : usize) (ret : t) :
result (hashmap_list_t t)
=
- hashmap_hash_map_get_mut_in_list_loop_back t key ls ret
+ hashmap_hash_map_get_mut_in_list_loop_back t ls key ret
(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
let hashmap_hash_map_get_mut_fwd
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 1b141d64..8cdc6e2c 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -42,7 +42,7 @@ let get_elem_mut_decreases (x : usize) (ls : list_t usize) : nat = admit ()
(** [loops::get_elem_shared]: decreases clause *)
unfold
-let get_elem_shared_decreases (x : usize) (slots : vec (list_t usize))
+let get_elem_shared_decreases (slots : vec (list_t usize)) (x : usize)
(ls : list_t usize) (ls0 : list_t usize) : nat =
admit ()
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index 57849896..a03f0302 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -43,8 +43,8 @@ let get_elem_mut_decreases (x : usize) (ls : list_t usize) : list_t usize = ls
(** [loops::get_elem_shared]: decreases clause *)
unfold
-let get_elem_shared_decreases (x : usize) (v : vec (list_t usize))
- (l : list_t usize) (ls : list_t usize) : list_t usize =
+let get_elem_shared_decreases (slots : vec (list_t usize)) (x : usize)
+ (ls : list_t usize) (ls0 : list_t usize) : list_t usize =
ls
(** [loops::list_nth_mut_loop_with_id]: decreases clause *)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index ca918e35..e8fb89e9 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -222,13 +222,13 @@ let get_elem_mut_back
(** [loops::get_elem_shared] *)
let rec get_elem_shared_loop_fwd
- (x : usize) (slots : vec (list_t usize)) (ls : list_t usize)
+ (slots : vec (list_t usize)) (x : usize) (ls : list_t usize)
(ls0 : list_t usize) :
- Tot (result usize) (decreases (get_elem_shared_decreases x slots ls ls0))
+ Tot (result usize) (decreases (get_elem_shared_decreases slots x ls ls0))
=
- begin match ls0 with
+ begin match ls with
| ListCons y tl ->
- if y = x then Return y else get_elem_shared_loop_fwd x slots ls tl
+ if y = x then Return y else get_elem_shared_loop_fwd slots x tl ls0
| ListNil -> Fail Failure
end
@@ -237,7 +237,7 @@ let get_elem_shared_fwd
(slots : vec (list_t usize)) (x : usize) : result usize =
begin match vec_index_fwd (list_t usize) slots 0 with
| Fail e -> Fail e
- | Return l -> get_elem_shared_loop_fwd x slots l l
+ | Return l -> get_elem_shared_loop_fwd slots x l l
end
(** [loops::id_mut] *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 12:48:20 +0000