Re: [isabelle] Bool cpo

Hello, thank you for your help, it was sucessfully proven and this issue is closed.

> From: s57076 at
> To: isabelle-users at
> Date: Tue, 27 Oct 2015 16:01:46 +0200
> Subject: 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.