Re: [isabelle] Problem with unfolding definitions while instantiating class
thank you for your answer.
> > And is it just me not understanding the type classes or overloading, or
> > it really strange that definitions of one type class use definitions of
> > another (stronger!) type class?
> What do you mean?
I expected the following behavior:
"fun"::(type, ccpo) does not care about definitions for "fun"::(type,
lattice) . Different type, different definitions.
If the type "inherits" from another type (i.e. is a supertype, as ccpo is
to order and sup), then it is wanted to "inherit" defintions .
I'm not sure if I am thinking to object oriented.
I thought locals introduce some sort of namespace, which could be used to
differentiate between different Sup definitions for different types.
> > I would also be grateful for explanations why it doesn't work, or why I
> > trying in a wrong direction.
> As Dave said, it is not your fault, the setup in Main is not fine-grained
> enough. You can modify Complete_Lattice as follows to make it work, but
> theories will no longer work with the distribution: replace the block [...]
Thank you for the tip, but I don't want to modify the distribution
theories. I was hoping more for something lika a "redefine" command inside
of a type instantiation.
Just out of curiosity, is there a place where I could vote for a change of
Complete_lattices.thy? And would it be a complete waste of time to do so?
> PS Do not import individual theories that are part of Main (like
> Complete_Partial_Order), start from Main instead. Otherwise you get some
> fragment of Main with unpredictable behaviour.
> I was hoping to not load Complete_lattices and its definitions this way,
and thereby be prompted to define Sup_fun by myself.
instantiation "fun" :: (type, ccpo) sup
threw the error
Conflict of type arities:
fun :: (type, ccpo) sup and
fun :: (type, lattice) sup
I solved my other problem, how to access the definition for chain while
instantiating pcpo, by instantiating cpo first, where the defintion was
My (unmet) expectation was that either I am prompted to define, or it is
defined (and the definition accessible).
This archive was generated by a fusion of
Pipermail (Mailman edition) and