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

From Core Require Import Core_Base_interface_Coerce.
Export Core_Base_interface_Coerce.

From Core Require Import Core_Base.
Export Core_Base.



From Core Require Import Core_Ops.
Export Core_Ops.

(* NotImplementedYet *)

(* NotImplementedYet *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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