(* 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. *)

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

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

From Core Require Import Core_Primitive.
Export Core_Primitive.

From Core Require Import Core_Cmp.
Export Core_Cmp.

From Core Require Import Core_Convert.
Export Core_Convert.

(* NotImplementedYet *)

(* NotImplementedYet *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(* 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_41'" := (impl_41). *)
