Library Corelib.Init.Number

Decimal or Hexadecimal numbers

Require Import Decimal Hexadecimal.

Variant uint := UIntDecimal (u:Decimal.uint) | UIntHexadecimal (u:Hexadecimal.uint).

Variant signed_int := IntDecimal (i:Decimal.int) | IntHexadecimal (i:Hexadecimal.int).

Variant number := Decimal (d:Decimal.decimal) | Hexadecimal (h:Hexadecimal.hexadecimal).

Scheme Equality for uint.
Scheme Equality for int.
Scheme Equality for number.

Register uint as num.num_uint.type.
Register int as num.num_int.type.
Register number as num.number.type.

Pseudo-conversion functions used when declaring Number Notations on uint and int.

Definition uint_of_uint (i:uint) := i.
Definition int_of_int (i:int) := i.

Module NumberNotations.
  Number Notation Number.uint Number.uint_of_uint Number.uint_of_uint
    : hex_uint_scope.
  Number Notation Number.int Number.int_of_int Number.int_of_int
    : hex_int_scope.

  Number Notation Number.uint Number.uint_of_uint Number.uint_of_uint
    : dec_uint_scope.
  Number Notation Number.int Number.int_of_int Number.int_of_int
    : dec_int_scope.
End NumberNotations.