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

From Core Require Import Core_Clone.
Export Core_Clone.

Notation "'t_Positive'" := positive.
Notation "'t_POSITIVE'" := positive.
Notation "'POSITIVE_XH'" := xH.
Notation "'POSITIVE_XO'" := xO.
Notation "'POSITIVE_XI'" := xI.

Definition positive_from_int (x : t_HaxInt) `{Hpos : x <> N0} : t_Positive :=
  match x return x <> N0 -> _ with | N0 => fun Hpos => False_rect _ (Hpos eq_refl) | Npos p => fun _ => p end Hpos.

Definition positive_to_int (s : t_Positive) : t_HaxInt := Npos s.

Definition xH : t_Positive := xH.
Definition xI (s : t_Positive) : t_Positive := xI s.
Definition xO (s : t_Positive) : t_Positive := xO s.

Definition match_positive (s : t_Positive) : t_POSITIVE := s.
