(* File automatically generated by Hacspec *)
From Coq Require Import ZArith.
Require Import List.
Import List.ListNotations.
Open Scope Z_scope.
Open Scope bool_scope.
Require Import Ascii.
Require Import String.
Require Import Coq.Floats.Floats.
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.

(* From Core Require Import Core. *)

From Core Require Import Core_Num.
Export Core_Num.



From Core Require Import Core_Ops_Index_range.
Export Core_Ops_Index_range.

From Core Require Import Core_Ops_Range.
Export Core_Ops_Range.

From Core Require Import Core_Primitive.
Export Core_Primitive.

(* From Core Require Import Core_Iter (t_IntoIterator). *)
(* Export Core_Iter (t_IntoIterator). *)

From Core Require Import Core_Clone.
Export Core_Clone.

From Core Require Import Core_Base.
Export Core_Base.

(* From Core Require Import hax_lib. *)
(* Export hax_lib. *)

Record t_IntoIter (v_T : Type) (v_N : t_usize) `{t_Sized (v_T)} : Type :=
  {
    IntoIter_f_data : t_Array ((v_T)) (v_N);
    IntoIter_f_alive : t_IndexRange;
  }.
Arguments Build_t_IntoIter (_) (_) {_}.
Arguments IntoIter_f_data {_} {_} {_}.
Arguments IntoIter_f_alive {_} {_} {_}.
#[export] Instance settable_t_IntoIter `{v_T : Type} `{v_N : t_usize} `{t_Sized (v_T)} : Settable _ :=
  settable! (Build_t_IntoIter v_T v_N) <IntoIter_f_data; IntoIter_f_alive>.
