Improve the order of the loop input parameters

2 files changed, 12 insertions, 12 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] *)