title: DedekindReals Requirements author:
- Ivo List status: Draft changes:
- 2019-03-21: Initial draft ...
User shall be able to describe a real number using two formulas describing lower and upper part of the cut.
Rationale: Provide a general way to enter a real number while keeping enough information to compute it. Don't provide or fix the method of computation.
Verification:
Source: Usecases: Computation and Expressiveness
User shall be able to enter following formulas:
- constant formulas: \top, \bot
- connectives: \land, \lor
Rationale:
Verification:
Source:
For an expression describing a real number, evaluation to given precision shall be possible.
Rationale:
Verification:
Source: Usecases: Computation and Expressiveness
Intervals shall be printed with minimal number of characters.
Rationale:
Verification: