Рассмотрим следующий надуманный пример объявления локали в Изабель:
locale x =
fixes f :: "'a ⇒ 'a"
assumes "f ∘ f = f"
locale y = x +
fixes g :: "'a ⇒ 'b"
begin
abbreviation h :: "'a ⇒ 'b" where "h ≡ g ∘ f"
end
Это невозможно, потому что 'a в локали x отличается от 'a в локали y. Как я могу сказать Изабель, что аргумент g должен иметь тот же тип, что и аргумент и результат f?