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:
 > defs
 >   funB_def   : "funB == lftsnd (funA :: 'a => (unit => unit) * ('d => 'e))"

An alternative is to parametrise funB with the types not mentioned.
For example

    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.

Best wishes,

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