Skip to content

Real vs Int printing

In a meeting with @hjsc @hbarbosa we decided that reals should always be printed with a decimal point. So a constant 1 is never a real.

Copied from @hbarbosa summary in the Alethe zulip:

After some discussion, the proposal is, for Alethe:

    numerals are integers
    decimals are reals
    reals can be written also in "GMP notation", i.e., [-]<numeral>/<numeral>

This needs to be added to the Standard.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information