*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Changing the arity of a term in ML*From*: Michael Chan <mchan at inf.ed.ac.uk>*Date*: Sun, 22 Jul 2012 17:57:18 +0100*In-reply-to*: <CAP0k5J5G4mSF0KPB6RASzbjEhF9poNRN9x2GUZeAoiCDRX-VSQ@mail.gmail.com>*References*: <CAP0k5J5G4mSF0KPB6RASzbjEhF9poNRN9x2GUZeAoiCDRX-VSQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:7.0.1) Gecko/20110929 Thunderbird/7.0.1

Hi John,

HTH Michael On 22/07/12 07:11, John Munroe wrote:

Hi, Say, given the terms val trm = @{term "%(a::nat => nat) b. a = b"} val arg = @{term "c::nat=>nat"} val arg' = @{term "d::nat=>bool"} if I'd like to create a new term in ML, which is essentially the same as "trm $ arg' " but 'a' and 'b' are to have the type "nat => bool" instead, I could change the type of every term in the trm part to dummyT (call it trm') and call Syntax.check_term on "trm' $ arg' " to reconstruct the types for the trm' part. Now, what if I want to decrease the arity of "a" and "b", e.g., from "nat => nat" to "nat"? I can't seem to use the same method. In trm, the = operator takes two lambda abstracted terms as arguments, but if 'a' and 'b' are to be of type 'nat', then = should take two bound variables instead. Is there a nice way to manipulate the type in this kind of situations such that the arity is decreased? Thanks a lot for the time. John

-- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

**References**:**[isabelle] Changing the arity of a term in ML***From:*John Munroe

- Previous by Date: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Date: Re: [isabelle] Isabelle/jedit
- Previous by Thread: [isabelle] Changing the arity of a term in ML
- Next by Thread: [isabelle] Isabelle/jedit
- Cl-isabelle-users July 2012 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