Library Coq.Numbers.Cyclic.Int63.PrimInt63

Require Export CarryType.


Variant pos_neg_int63 := Pos (d:int) | Neg (d:int).
Definition id_int : int -> int := fun x => x.
Record int_wrapper := wrap_int {int_wrap : int}.
Definition printer (x : int_wrapper) : pos_neg_int63 := Pos (int_wrap x).
Definition parser (x : pos_neg_int63) : option int :=
  match x with
  | Pos p => Some p
  | Neg _ => None
  end.

Module Import Int63NotationsInternalA.
Delimit Scope int63_scope with int63.
End Int63NotationsInternalA.

Module Export PrimInt63Notations.
  Export Int63NotationsInternalA.
End PrimInt63Notations.