Re: [isabelle] Bool cpo
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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and