[isabelle-dev] Towards the next release

[Florian Haftmann]

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

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