(* 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_Primitive.
Export Core_Primitive.



From Core Require Import Core_Slice_Iter.
Export Core_Slice_Iter.

From Core Require Import Core_Convert.
Export Core_Convert.

(* NotImplementedYet *)

(* NotImplementedYet *)

Definition impl__iter `{v_T : Type} `{t_Sized (v_T)} `{t_Clone (v_T)} (self : t_Slice ((v_T))) : t_Iter ((v_T)) :=
  impl__new (self).

Definition impl__len `{v_T : Type} `{t_Sized (v_T)} `{t_Clone (v_T)} (self : t_Slice ((v_T))) : t_usize :=
  From_f_from (len (Clone_f_clone (Slice_f_v self))).

Definition impl__is_empty `{v_T : Type} `{t_Sized (v_T)} `{t_Clone (v_T)} (self : t_Slice ((v_T))) : bool :=
  PartialEq_f_eq (impl__len (self)) (Build_t_usize (Build_t_U64 0%N)).
