[isabelle] Comparing polymorphic functions



Hello

With the "=" operator, I can do comparisons like:

consts
f :: "'a1 => 'a2"
g :: "'a1 => 'a2 => 'a3"

lemma "f = g"
...

But in HOL.thy, it's defined as

eq            :: "['a, 'a] => bool"               (infixl "=" 50)

Since Isabelle/HOL is only simply typed with type variables, how come 'a can
be instantiated to 'a1 => 'a2 and 'b can be instantiated to 'a1 => 'a2 =>
'a3, even they are of different arities? However, if f was

f :: "real => real"

then type unification fails with "f = g".

Thx




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