Very good! This is very convenient.
On 01/06/16 21:42, Makarius wrote:
*** ML ***
* Structure Rat for rational numbers is now an integral part of
Isabelle/ML, with special notation @int/nat or @int for numerals (an
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
printing. Standard operations on type Rat.rat are provided via ad-hoc
overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to
use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
superseded by General.Div.
This refers to Isabelle/c7de5b311909, which also contains the updated
documentation.
The antiquotation syntax @int/nat for @{Pure.rat argument} is stretching
the existing syntax very little, see 921a5be54132. Further changesets in
the vicinity clean up rat.ML is various repects -- it is surprising how
many details can be missing in such a small module.
I have compared it with the MyRat implementation by Manuel Eberl
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-April/msg00002.html
as well as rat.ML in https://bitbucket.org/lcpaulson/metitarski
b11e8139b880 (where a comment says that it goes back to John Harrison).
Further comments? Anything missing?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
