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

Class t_From (v_Self : Type) (v_T : Type) (* `{t_Sized (v_Self)} `{t_Sized (v_T)} *) : Type :=
  {
    From_f_from : v_T -> v_Self;
  }.
Arguments t_From (_) (_) (* {_} {_} *).

#[global] Instance t_From_46353410 `{v_T : Type} (* `{t_Sized (v_T)} *) : t_From ((v_T)) ((v_T)) :=
  {
    From_f_from := fun  (t : v_T)=>
      t;
  }.

Class t_Into (v_Self : Type) (v_T : Type) (* `{t_Sized (v_Self)} `{t_Sized (v_T)} *) : Type :=
  {
    Into_f_into : v_Self -> v_T;
  }.
Arguments t_Into (_) (_) (* {_} {_} *).

#[global] Instance t_Into_730689925 `{v_T : Type} `{v_U : Type} (* `{t_Sized (v_T)} `{t_Sized (v_U)} *) `{t_From (v_U) (v_T)} : t_Into ((v_T)) ((v_U)) :=
  {
    Into_f_into := fun  (self : v_T)=>
      From_f_from (self);
  }.
