[isabelle] "Coercion inference failed"



Hello all,

Does anyone know why the following gives an error saying: "Coercion
inference failed: weak unification of subtype constraints fails"?

axiomatization
f :: "'a => 'b" and
g :: "nat => nat" where
ax : "f = g"

However,

lemma "f = g"

successfully goes through without giving an error.

Any help will be appreciated.

Eg




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