On 12/06/2016 18:22, Florian Haftmann wrote:
Thus I would like to understand why we cannot reuse Sup etc in HOLCF
like we do for all the other variants of lattices we have. We would
probably need a suitable type class because at the moment lub is
unrestricted.
For each type class, per type
> Thus I would like to understand why we cannot reuse Sup etc in HOLCF
> like we do for all the other variants of lattices we have. We would
> probably need a suitable type class because at the moment lub is
> unrestricted.
For each type class, per type constructor there is at most *one*
On 11/06/2016 21:26, Florian Haftmann wrote:
For the moment I think bold syntax in the first choice. In the middle
run I would suggest to have a closer look at HOLCF/Porder.thy to see
whether something can be done to integrate it more with the standard
type classes; a least it formalizes a
