Improve the order of the loop input parameters

3 files changed, 12 insertions, 12 deletions

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