> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
