Re: [isabelle] Bool cpo
Hello, thank you for your help, it was sucessfully proven and this issue is closed.
> From: s57076 at hotmail.com
> To: isabelle-users at cl.cam.ac.uk
> 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