[isabelle] problem with locales



I have the following two locales:

locale node =
  fixes nil :: "'node"
  assumes infinite: "¬ finite (UNIV::'node set)"
begin
  definition "domain f = {x :: 'node .  - (f x = (nil::'node))}"
end

locale list = node +
  fixes "next" :: "'node => 'node"
  fixes val :: "'node => 'node"
  assumes "next (nil::'node) = nil"

These locales generate error "Type unification failed". If I drop the
definition from the first locale then I do not get this message.

More generally. Is there a standard mechanism to enforce
the type 'node from the first locale to be the same as the
type node from the second locale?

Best regards,

Viorel





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.