[isabelle] Types for variables


I got a question about types for variables: can they have types? For
example, if I want to prove if a binary function that takes in a Natural and
an Integer can be instantiated:

F :: "[nat,int] => int"
ax: "F p t = G p t"

lemma lem1: "EX f.f x y = G p t"
using ax

where f should be typed (perhaps x and y as well).

Thanks very much

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