Re: [isabelle] Types for variables
John Munroe wrote:
> 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
Isabelle infers the type automatically to the most generic type in an
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,
> 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