[isabelle-dev] Quotient example with partiality?
makarius at sketis.net
Mon Nov 28 22:32:00 CET 2011
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.
More information about the isabelle-dev