[isabelle-dev] Quotient example with partiality?

[Florian Haftmann]

Hi all,

I'm asking myself the question how one would define rational numbers
using the quotient package.  The key issue is that the equivalence
relation here is partial, ruling out denominators of value zero.  In the
Isabelle reference manual I can find »partial:« in a syntax diagram but
not any concrete example in the distribution.

The reason why I ask is that I want to understand if *every* typedef
specification can be written as quotient type specification (in a
straightforward manner).  If yes, quotient_type could replace typedef in
user space in general, and many recent requests for adjusting the
user-space behavior of typedef would then rather apply to quotient_type.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.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: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20111128/dabbacac/attachment.asc>