Module `NumTok`

Numbers in different forms: signed or unsigned, possibly with fractional part and exponent.

Numbers are represented using raw strings of (hexa)decimal literals and a separate sign flag.

Note that this representation is not unique, due to possible multiple leading or trailing zeros, and -0 = +0, for instances. The reason to keep the number exactly as it was parsed is that specific notations can be declared for specific numbers (e.g. Notation "0" := False, or Notation "00" := (nil,nil), or Notation "2e1" := ...). Those notations override the generic interpretation as number. So, one has to record the form of the number which exactly matches the notation.

type sign =

| SPlus

| SMinus

type num_class =

| CDec

| CHex

type 'a exp =

| EDec of 'a

| EBin of 'a

String representation of a natural number

module UnsignedNat : sig ... end

String representation of a signed natural number

module SignedNat : sig ... end

Unsigned decimal numbers

module Unsigned : sig ... end

Signed decimal numbers

module Signed : sig ... end