Re: [isabelle] type inference in HOL
Florian Haftmann writes:
> The point is that you don't state anything about the type parameters 'b
> and 'c of funA in funB_def since they do not occur on the left hand side
> of funB_def; you have to instantiate them:
> funB_def : "funB == lftsnd (funA :: 'a => (unit => unit) * ('d => 'e))"
An alternative is to parametrise funB with the types not mentioned.
lftsnd :: "('a => 'b * 'c) => 'a => 'c"
funA :: "'a => ('b => 'c) * ('d => 'e)"
lftsnd_def : "lftsnd f x == snd (f x)"
funB_def: "funB TYPE('b) TYPE('c) == lftsnd (funA::'a=>('b=>'c)*('d=>'e))"
The reason why all type-variables of a right-hand side
of a definition have to occur on the left-hand side as
well is that otherwise one can write down definitions
that lead to inconsistencies.
This archive was generated by a fusion of
Pipermail (Mailman edition) and