
(* 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_Marker.
Export Core_Marker.

From Core Require Import Core_Option.
Export Core_Option.

From Core Require Import Core_Primitive.
Export Core_Primitive.

From Core Require Import Core_Ops_Function.
Export Core_Ops_Function.

Class t_Iterator (v_Self : Type) : Type :=
  {
    Iterator_f_Item : Type;
    _H_Sized :: `{t_Sized (Iterator_f_Item)};
    Iterator_f_next : v_Self -> (v_Self*t_Option ((Iterator_f_Item)));
    Iterator_f_size_hint : v_Self -> (t_usize*t_Option ((t_usize)));
    Iterator_f_fold (v_B : Type) (v_F : Type) `{t_Sized (v_B)} `{t_Sized (v_F)} `{t_Sized (v_Self)} `{t_FnMut (v_F) ((v_B*Iterator_f_Item))} `{_.(FnOnce_f_Output) = v_B} : v_Self -> v_B -> v_F -> v_B;
  }.
Arguments t_Iterator (_).
