Require Import Basics.Overture Basics.Numerals.Decimal Basics.Numerals.Hexadecimal.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** * Decimal or Hexadecimal numbers *)

Variant uint : Type0 := UIntDec (u:Decimal.uint) | UIntHex (u:Hexadecimal.uint).

Variant int : Type0 := IntDec (i:Decimal.int) | IntHex (i:Hexadecimal.int).

Variant numeral : Type0 := Dec (d:Decimal.decimal) | Hex (h:Hexadecimal.hexadecimal).

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

(** 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.

(* Parsing / printing of decimal numbers *)
Number Notation uint uint_of_uint uint_of_uint : dec_uint_scope.
Number Notation int int_of_int int_of_int : dec_int_scope.