3 ms·
Very interesting. How would this language, or similar systems, deal with lemmas that are true for real numbers but not always true for floats?
by leephillips 3y ago
Very interesting. How would this language, or similar systems, deal with lemmas that are true for real numbers but not always true for floats?
- lolinder 3y agoIn Dafny's case, they don't: `real` is compiled to a representation like BigRational that actually behaves like a real number. In JavaScript it uses bignumber.js: https://github.com/MikeMcl/bignumber.js https://github.com/MikeMcl/bignumber.js