[isabelle-dev] Towards the next release
florian.haftmann at informatik.tu-muenchen.de
Wed Apr 18 20:14:30 CEST 2012
> The overloading rules are quite tricky. I don't understand why the first instantiation requires a definition of sup_hf (including the type in the constant name), while the second one simply requires a definition of minus. Perhaps because there is an explicit type in the first instantiation and not on the second one? In any event, if the user gets wrong, a warning would be appropriate. And I hope that wouldn't be difficult to implement.
> instantiation hf :: sup
> definition sup_hf :: "hf \<Rightarrow> hf \<Rightarrow> hf"
> where "sup_hf a b = ..."
> instantiation hf :: minus
> definition minus_hf where
> "minus A B = ...
> instance proof
the rules are roughly as follows:
* Given a class parameter foo to be instantiated to a type bar, the
corresponding parameter name for defining foo on bar is foo_bar; this
can also be inspected using the print_context command inside the
* Given a class parameter foo with type T[?'a], each of its appearances
at type T[('a, …, 'z) bar] is substituted by foo_bar.
Hope this helps,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev