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.
Exact arithmetic operations
Comparison
Exotic operations