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

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

  defs
    lftsnd_def : "lftsnd f x == snd (f x)"

  constdefs
    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,
Christian





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