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

From Core Require Import Core_Cmp.
Export Core_Cmp.

From Core Require Import Core_Base.
Export Core_Base.

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

From Core Require Import Core_Base_interface_Int.
Export Core_Base_interface_Int.

From Core Require Import Core_Array_Rec_bundle_579704328.
Export Core_Array_Rec_bundle_579704328.

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

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

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

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

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

Notation "'impl_3__cast'" := (cast).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(* NotImplementedYet *)

(* NotImplementedYet *)

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

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

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

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

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

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

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

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

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

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

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

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

(* NotImplementedYet *)

(* NotImplementedYet *)

(* NotImplementedYet *)

(* NotImplementedYet *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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