*To*: cl-isabelle-users at lists.cam.ac.uk, jpw48 at cam.ac.uk*Subject*: Re: [isabelle] Lifting a partial definition to a quotient type*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Tue, 12 Mar 2013 20:11:53 +0100*In-reply-to*: <980F6EE1-48DD-48EE-A996-BDA66CFB0630@cam.ac.uk>*Organization*: TU Munich*References*: <980F6EE1-48DD-48EE-A996-BDA66CFB0630@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130221 Thunderbird/17.0.3

Hi John, Am 12.03.2013 15:27, schrieb John Wickerson: > Hi, I just wanted to alert the Quotient people to the following question that has recently appeared on Stack Overflow, on which they might have an opinion... > > http://stackoverflow.com/questions/15347913/lifting-a-partial-definition-to-a-quotient-type this is slightly off-topic, but note that HOL is total. I. e. definition "X ∩ Y = {} ⟹ disj_union X Y ≡ X ∪ Y" yields a guarded equation, but on the foundational definition level disj_union is equivalent to union. I'm skeptic whether such »partiality« is inherent to your example -- very likely in can be circumvented. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Lifting a partial definition to a quotient type***From:*John Wickerson

**References**:**[isabelle] Lifting a partial definition to a quotient type***From:*John Wickerson

- Previous by Date: [isabelle] Lifting a partial definition to a quotient type
- Next by Date: Re: [isabelle] Lifting a partial definition to a quotient type
- Previous by Thread: [isabelle] Lifting a partial definition to a quotient type
- Next by Thread: Re: [isabelle] Lifting a partial definition to a quotient type
- Cl-isabelle-users March 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list