(* 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_Base_Spec_Haxint.
Export Core_Base_Spec_Haxint.

Notation "'t_Unary'" := nat.

Notation "'t_UNARY'" := nat.
Notation "'UNARY_ZERO'" := O.
Notation "'UNARY_SUCC'" := S.

Definition unary_from_int (x : t_HaxInt) : t_Unary := N.to_nat x.
Definition unary_to_int (s : t_Unary) : t_HaxInt := N.of_nat s.

Definition pred (x : t_Unary) : t_Unary := Nat.pred x.

Definition match_unary (s : t_Unary) : t_UNARY := s.

Definition succ (x : t_Unary) : t_Unary := S x.
