Floating-point numbers

Requires special terms (floatingPointNumbers) that cannot be implemented in Leibniz itself. Floating-point number literals must contain either a decimal point or an exponent to distinguish them from Integers. Examples of floating-point numbers: 1.0, 1.0, -2.5, 42.0, 0.03.

Most programming languages pretend that floating-point numbers are equivalent to real numbers, and in particular a superset of the integers. They thus convert integers to floating-point numbers automatically when useful. This is the cause of many problems because the floating-point numbers are really a subset of the rational numbers that is distinct from, but has an overlap with, the integers.

In Leibniz, floating-point numbers are completely separate from the integer - rational number - real number categories. There is no automatic conversion in either direction at any time.

The sort for IEEE-754 double-precision binary floating-point number is FP64. It has three subsorts:
- FP64.number ⊆ FP64 for number values
- FP64.inf ⊆ FP64 for the infinities
- FP64.NaN ⊆ FP64 for the "not-a-number" values

The current implementation of Leibniz does not contain other precisions, nor IEEE decimal floating-point numbers.