Re: [isabelle] Bool cpo



Correction:
to make set a cpo, its sufficient to make bool a cpo.
 If one defines the "â" operator as the "-->" operator on booleans, one obtains a partial order.
 instantiation bool :: pobegin definition less_bool_def: "(op â) = (op -->)"instanceby (intro_classes, unfold less_bool_def, safe)end

 This induces an order on sets, which corresponds to the "â" operator. 

 lemma less_set_eq: "(op â) = (op â)"

 But this lemma is not accepted by giving this error message:
 ---Type unification failed: No type arity set :: below---

 Can you help me?

By the way, i am aware of this answer of a similiar question:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-September/msg00010.html


 Many thanks! 











> From: s57076 at hotmail.com
> To: isabelle-users at cl.cam.ac.uk
> Date: Mon, 26 Oct 2015 21:27:00 +0200
> Subject: [isabelle] Bool cpo
> 
> Hello,
> to make set a cpo, its sufficient to make bool a cpo.
> If one defines the "â" operator as the "â" operator on booleans,  one obtains a partial order.
> instantiation bool :: pobegin  definition less_bool_def: "(op â) = (op â)"instanceby (intro_classes, unfold less_bool_def, safe)end
> This induces an order on sets, which corresponds to the  "â" operator. 
> lemma less_set_eq: "(op â) = (op â)"
> But this lemma is not accepted by giving this error message:
> ---Type unification failed: No type arity set :: below---
> Can you help me?
> Many thanks! 		 	   		  
 		 	   		  


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