(* 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 "'t_Seq'" := list.

Notation "'t_LIST'" := list.
Notation "'LIST_NIL'" := nil.
Notation "'LIST_CONS'" := cons.

Notation "'nil'" := nil.
Notation "'cons'" := (fun x y => cons y x).

Definition match_list {T} (x : t_Seq T) : t_LIST T := x.
