Improve the order of the loop input parameters

3 files changed, 16 insertions, 16 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] *)