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.