[isabelle] Comparing polymorphic functions
With the "=" operator, I can do comparisons like:
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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and