Hi all, > 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 > begin > > definition sup_hf :: "hf \<Rightarrow> hf \<Rightarrow> hf" > where "sup_hf a b = ..." > > instantiation hf :: minus > begin > 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
instantiation block.
* 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,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
