[isabelle] type inference in HOL



The following left me puzzled:

consts
lftsnd  :: "('a => ('b*'c)) => ('a => 'c)"
funA    :: "'a => (('c => 'e)*('d => 'f))"
funB    :: "'a => 'h => 'k"

defs
lftsnd_def : "lftsnd f x == snd (f x)"
funB_def   : "funB == lftsnd funA"

ô*** Extra type variables on rhs: "'d", "'e"
*** The error(s) above occurred in definition "funC_def":
***   "funC == funB funA"
*** At command "defs".õ

Can anybody spot the problem?

Regards,

Paolo Torrini







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