new type: Decimal
florianschanda opened this issue · 0 comments
florianschanda commented
Add support for decimal (rational) numbers.
In the Python API they would come out as an instance of rational, not float, in order to preserve precision.
Expressions with Integer and Decimal are not compatible and you need to explicitly cast between them, for example:
Decimal(i + 1) + 0.3 < d
Semantics for rounding are the classic ones (round nearest away).