# Re: [isabelle] Types for variables

John Munroe wrote:
> Hi,
>
> 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:
>
> consts
> F :: "[nat,int] => int"
> axioms
> ax: "F p t = G p t"
>
> lemma lem1: "EX f.f x y = G p t"
> using ax
>
>
Isabelle infers the type automatically to the most generic type in an
ML-like fashion.
You can constrain the type of any expression and variable by:
exp :: type, i.e.
EX f :: nat => int => int. f x y = G p t
the types of x and y are then inferred automatically to nat and int.
Usually you will have to put parenthesis around the type constraint, i.e.
EX f. f (x::nat) (y::int) = G p t
If you are unsure about the actual types, activate the option "Show
types" (In the Isabelle->Settings menu of PG)
Hope this helps,
Peter
> where f should be typed (perhaps x and y as well).
>
> Thanks very much
> John
>

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