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

Require Import Core_Primitive.
Export Core_Primitive.

(* Handwritten *)

Coercion Build_t_i8 : t_I8 >-> t_i8.
Coercion Build_t_I8 : Z >-> t_I8.

Coercion Build_t_i16 : t_I16 >-> t_i16.
Coercion Build_t_I16 : Z >-> t_I16.

Coercion Build_t_i32 : t_I32 >-> t_i32.
Coercion Build_t_I32 : Z >-> t_I32.

Coercion Build_t_i64 : t_I64 >-> t_i64.
Coercion Build_t_I64 : Z >-> t_I64.

Coercion Build_t_i128 : t_I128 >-> t_i128.
Coercion Build_t_I128 : Z >-> t_I128.

Coercion Build_t_isize : t_I64 >-> t_isize.

Coercion Build_t_u8 : t_U8 >-> t_u8.
Coercion Build_t_U8 : N >-> t_U8.

Coercion Build_t_u16 : t_U16 >-> t_u16.
Coercion Build_t_U16 : N >-> t_U16.

Coercion Build_t_u32 : t_U32 >-> t_u32.
Coercion Build_t_U32 : N >-> t_U32.

Coercion Build_t_u64 : t_U64 >-> t_u64.
Coercion Build_t_U64 : N >-> t_U64.

Coercion Build_t_u128 : t_U128 >-> t_u128.
Coercion Build_t_U128 : N >-> t_U128.

Coercion Build_t_usize : t_U64 >-> t_usize.

Coercion Z.to_N : Z >-> N.
