> * 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?
Very fine. Indeed rat.ML has been one of my first Isabelle playgrounds, and I did not have much experience then. One could regard the dedicated literal syntax for rationals a little bit oversophisticated; maybe an infix // for Rat.make would serve better. Or we could A matter of personal taste, though. Cheers, Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev