[isabelle-dev] NEWS: Rat in Isabelle/ML

[Florian Haftmann]

> * 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160601/4d8f4513/attachment.sig>