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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
