(* 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_Arith (t_Add). *)
(* Export Core_Ops_Arith (t_Add). *)

(* From Core Require Import Core_Ops_Arith (t_Div). *)
(* Export Core_Ops_Arith (t_Div). *)

(* From Core Require Import Core_Ops_Arith (t_Mul). *)
(* Export Core_Ops_Arith (t_Mul). *)

(* From Core Require Import Core_Ops_Arith (t_Neg). *)
(* Export Core_Ops_Arith (t_Neg). *)

(* From Core Require Import Core_Ops_Arith (t_Rem). *)
(* Export Core_Ops_Arith (t_Rem). *)

(* From Core Require Import Core_Ops_Arith (t_Sub). *)
(* Export Core_Ops_Arith (t_Sub). *)

From Core Require Import Core_Ops_Arith.
Export Core_Ops_Arith.



(* From Core Require Import Core_Ops_Bit (t_BitAnd). *)
(* Export Core_Ops_Bit (t_BitAnd). *)

(* From Core Require Import Core_Ops_Bit (t_BitOr). *)
(* Export Core_Ops_Bit (t_BitOr). *)

(* From Core Require Import Core_Ops_Bit (t_BitXor). *)
(* Export Core_Ops_Bit (t_BitXor). *)

(* From Core Require Import Core_Ops_Bit (t_Not). *)
(* Export Core_Ops_Bit (t_Not). *)

(* From Core Require Import Core_Ops_Bit (t_Shl). *)
(* Export Core_Ops_Bit (t_Shl). *)

(* From Core Require Import Core_Ops_Bit (t_Shr). *)
(* Export Core_Ops_Bit (t_Shr). *)

From Core Require Import Core_Ops_Bit.
Export Core_Ops_Bit.



From Core Require Import Core_Ops_Index.
Export Core_Ops_Index.



From Core Require Import Core_Ops_Range.
Export Core_Ops_Range.

(* From Core Require Import Core_Ops_Index_range (t_IndexRange). *)
(* Export Core_Ops_Index_range (t_IndexRange). *)

(* NotImplementedYet *)

(* NotImplementedYet *)

(* NotImplementedYet *)

(* NotImplementedYet *)

(* NotImplementedYet *)

(* NotImplementedYet *)
