[isabelle] Isabelle 2011 locales



Hello,

Could you explain me, why in the following example, Isabelle 2011
accepts command value "id2 1", but refuses command value "id1 1"
(with message like "1 is incompatible with type 'a") ?

(*-------------------------------------------------*)
theory LocaleTest imports Main
begin
locale test_loc = fixes f :: "'a \<Rightarrow> 'a"
begin

fun id1::"'a \<Rightarrow> 'a" where "id1 x = x"
fun id2::"'b \<Rightarrow> 'b" where "id2 x = x"

value "id2 1"

value "id1 1"

end
end
(*-------------------------------------------------*)

Ievgen Ivanov






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