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...
> 
> 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
Description: OpenPGP digital signature



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