On 11/28/2011 07:25 PM, Florian Haftmann wrote:
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.
Actually, the quotient package does more than an simple type definition.
It also defines some further constants.
many recent requests for adjusting the user-space behavior of typedef would
then rather apply to quotient_type.
Also, I do not see the clear advantage how the suggested change would
make the adjustments simpler.
I would rather imagine that the quotient_type command could be
assimilated by extending the typedef command to enable to hook the pre-
and post processing of quotient type into typedef.
Lukas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
