(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [hashmap_main]: templates for the decreases clauses *)
module HashmapMain.Clauses.Template
open Primitives
open HashmapMain.Types

#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"

(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: decreases clause
    Source: 'tests/src/hashmap.rs', lines 50:4-56:5 *)
unfold
let hashmap_HashMap_allocate_slots_loop_decreases (t : Type0)
  (slots : alloc_vec_Vec (hashmap_List_t t)) (n : usize) : nat =
  admit ()