diff options
Diffstat (limited to 'tests/hashmap/Hashmap.Clauses.Template.fst')
| -rw-r--r-- | tests/hashmap/Hashmap.Clauses.Template.fst | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tests/hashmap/Hashmap.Clauses.Template.fst b/tests/hashmap/Hashmap.Clauses.Template.fst index c1549e6b..2a3d9cb9 100644 --- a/tests/hashmap/Hashmap.Clauses.Template.fst +++ b/tests/hashmap/Hashmap.Clauses.Template.fst @@ -24,6 +24,10 @@ let hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t) (ls : list_t t) : nat = admit () +(** [core::num::u32::{8}::MAX] *) +let core_num_u32_max_body : result u32 = Return 4294967295 +let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body + (** [hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *) unfold let hash_map_move_elements_from_list_decreases (t : Type0) |