[isabelle-dev] Syntax for lattice operations?

[Florian Haftmann]

> 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*
instance.

If we use the standard HOL class hierarchy for HOLCF, we
would e.g. enforce the order on pairs to be component-wise due to the
required / given instance of cpo in HOLCF and hence rule out e.g.
lexicographic ordering on pairs.  Hence the use of a separate
type class hierarchy makes sense for that specific application.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160612/e9f35515/attachment.sig>