Re: [isabelle] Bool cpo

Hello Johannes

my exact question is:
While working in HOLCF(not HOL)...if I copy-paste the following class SetPcpo
in the HOLCF folder,
and run it, then I get at the following spot
lemma less_set_eq: "(op â) = (op â)"the following error: --Type unification failed: No type arity set :: below

Type error in application: incompatible operand type

Operator:  op = op â :: (??'a â ??'a â bool) â bool
Operand:   op â :: ??'b set â ??'b set â bool--1. Why is the error?
2. How do i prove here "instance bool :: cpo"   //notice that this is the class cpo of holcf, as in [Huf 11],  and not --hol ccpo--  3. How do i then prove "instance set :: (type) cpo"     
Thank you! 		 	   		  

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