(* 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_HaxInt'" := N.

Definition v_HaxInt_ONE : t_HaxInt := 1.
Definition v_HaxInt_TWO : t_HaxInt := 2.
Definition v_HaxInt_ZERO : t_HaxInt := 0.

Definition div2 (s : t_HaxInt) : t_HaxInt := s / 2.

Definition is_zero (s : t_HaxInt) : bool := match s with | N0 => true | _ => false end.

