diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 12 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 12 |
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] *) |