Library Coq.Numbers.Cyclic.Int63.PrimInt63
Require
Export
CarryType
.
Register
bool
as
kernel.ind_bool
.
Register
prod
as
kernel.ind_pair
.
Register
carry
as
kernel.ind_carry
.
Register
comparison
as
kernel.ind_cmp
.
Primitive
int
:= #
int63_type
.
Register
int
as
num.int63.type
.
Variant
pos_neg_int63
:=
Pos
(
d
:
int
) |
Neg
(
d
:
int
).
Register
pos_neg_int63
as
num.int63.pos_neg_int63
.
Declare Scope
uint63_scope
.
Definition
id_int
:
int
->
int
:=
fun
x
=>
x
.
Record
int_wrapper
:=
wrap_int
{
int_wrap
:
int
}.
Register
wrap_int
as
num.int63.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
.
Declare Scope
int63_scope
.
Module
Import
Int63NotationsInternalA
.
Delimit
Scope
int63_scope
with
int63
.
End
Int63NotationsInternalA
.
Module
Import
Uint63NotationsInternalA
.
Delimit
Scope
uint63_scope
with
uint63
.
Bind Scope
uint63_scope
with
int
.
End
Uint63NotationsInternalA
.
Primitive
lsl
:= #
int63_lsl
.
Primitive
lsr
:= #
int63_lsr
.
Primitive
land
:= #
int63_land
.
Primitive
lor
:= #
int63_lor
.
Primitive
lxor
:= #
int63_lxor
.
Primitive
asr
:= #
int63_asr
.
Primitive
add
:= #
int63_add
.
Primitive
sub
:= #
int63_sub
.
Primitive
mul
:= #
int63_mul
.
Primitive
mulc
:= #
int63_mulc
.
Primitive
div
:= #
int63_div
.
Primitive
mod
:= #
int63_mod
.
Primitive
divs
:= #
int63_divs
.
Primitive
mods
:= #
int63_mods
.
Primitive
eqb
:= #
int63_eq
.
Primitive
ltb
:= #
int63_lt
.
Primitive
leb
:= #
int63_le
.
Primitive
ltsb
:= #
int63_lts
.
Primitive
lesb
:= #
int63_les
.
Exact arithmetic operations
Primitive
addc
:= #
int63_addc
.
Primitive
addcarryc
:= #
int63_addcarryc
.
Primitive
subc
:= #
int63_subc
.
Primitive
subcarryc
:= #
int63_subcarryc
.
Primitive
diveucl
:= #
int63_diveucl
.
Primitive
diveucl_21
:= #
int63_div21
.
Primitive
addmuldiv
:= #
int63_addmuldiv
.
Comparison
Primitive
compare
:= #
int63_compare
.
Primitive
compares
:= #
int63_compares
.
Exotic operations
Primitive
head0
:= #
int63_head0
.
Primitive
tail0
:= #
int63_tail0
.
Module
Export
PrimInt63Notations
.
Export
Int63NotationsInternalA
.
Export
Uint63NotationsInternalA
.
End
PrimInt63Notations
.