*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Types for variables*From*: John Munroe <munddr at googlemail.com>*Date*: Wed, 2 Sep 2009 05:25:07 +0100

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 where f should be typed (perhaps x and y as well). Thanks very much John

**Follow-Ups**:**Re: [isabelle] Types for variables***From:*Peter Lammich

- Previous by Date: [isabelle] Defining a function on an inductively defined set.
- Next by Date: Re: [isabelle] Types for variables
- Previous by Thread: Re: [isabelle] Defining a function on an inductively defined set.
- Next by Thread: Re: [isabelle] Types for variables
- Cl-isabelle-users September 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list