[isabelle-dev] Quotient example with partiality?

[Makarius]

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