(* 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_Ops_Index.
Export Core_Ops_Index.

(* From Core Require Import Core_Ops_IndexMut. *)
(* Export Core_Ops (t_IndexMut). *)

From Core Require Import Core_Primitive.
Export Core_Primitive.

From Core Require Import Core_Array_Iter.
Export Core_Array_Iter.

Notation "'t_TryFromSliceError'" := (t_TryFromSliceError).

Notation "'TryFromSliceError_0'" := (TryFromSliceError_0).

(* NotImplementedYet *)

(* Notation "'impl_2'" := (impl_2). *)

(* Notation "'impl_1'" := (impl_1). *)

(* Notation "'impl'" := (impl). *)
