[isabelle-dev] Quotient example with partiality?
florian.haftmann at informatik.tu-muenchen.de
Mon Nov 28 19:25:19 CET 2011
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev