Re: [isabelle] Lifting a partial definition to a quotient type

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...

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



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.