On Mon, 28 Nov 2011, Florian Haftmann wrote:
I'm asking myself the question how one would define rational numbers
using the quotient package.
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.
How about datatype and record, then? I don't quite see why the
traditional Gordon-HOL style typedef should be supplanted in general.
I feel recently inclined to *remove* a few features from typedef, notably
the extra set definition and optional name arguments.
Independently to this, quotient_type can be made more popular, of course,
but this should involve a few more rounds of proper localization.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
