Library Coq.Init.Numeral
Decimal or Hexadecimal numbers
Require
Import
Decimal
Hexadecimal
.
Variant
uint
:=
UIntDec
(
u
:
Decimal.uint
) |
UIntHex
(
u
:
Hexadecimal.uint
).
Variant
int
:=
IntDec
(
i
:
Decimal.int
) |
IntHex
(
i
:
Hexadecimal.int
).
Variant
numeral
:=
Dec
(
d
:
Decimal.decimal
) |
Hex
(
h
:
Hexadecimal.hexadecimal
).
Scheme
Equality
for
uint
.
Scheme
Equality
for
int
.
Scheme
Equality
for
numeral
.
Pseudo-conversion functions used when declaring Numeral Notations on
uint
and
int
.
Definition
uint_of_uint
(
i
:
uint
) :=
i
.
Definition
int_of_int
(
i
:
int
) :=
i
.