Re: [isabelle] type inference in HOL



Dear Paolo,

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

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

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))"

will work.

Hope this helps
Florian
begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
	=0D=0A=
	http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
	nformatik_tu_muenchen_de.pgp=0D=0A=
	
x-mozilla-html:FALSE
url:http://isabelle.in.tum.de/~haftmann
version:2.1
end:vcard

Attachment: signature.asc
Description: OpenPGP digital signature



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