*To*: cl-isabelle-users at lists.cam.ac.uk, s.wong.731 at gmail.com*Subject*: Re: [isabelle] Constructing terms in ML*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Tue, 27 Sep 2011 11:20:29 +1000*In-reply-to*: <CAFU+7wNpPufNsDHggden5Wj_0JdhVvb6uzhBRpaE84OXbYHfFQ@mail.gmail.com>*References*: <CAFU+7wNpPufNsDHggden5Wj_0JdhVvb6uzhBRpaE84OXbYHfFQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.15) Gecko/20110419 Thunderbird/3.1.9

Hello Steve.

For instance ML {* let val T = @{typ 'a} in

*} Or the slightly shorter ML {* let val T = @{typ 'a} in

*} There are usually many different ways to do things. Here is another one, which may come as something of a surprise: ML {* let val T = @{typ 'a} in

*}

Yours, Thomas. On 27/09/11 09:04, Steve Wong wrote:

Hi all, I'm trying to construct the term for "ALL x y. x = y". I know I could just use Syntax.read_term, but what if I want to construct it term by term using the constructor functions? I see that the term should look something like: Const ("HOL.All", "('a => HOL.bool) => HOL.bool") $ Abs ("x", "'a", Const ("HOL.All", "('a => HOL.bool) => HOL.bool") $ Abs ("y", "'a", Const ("HOL.eq", "'a => 'a => HOL.bool") $ Bound 1 $ Bound 0)) Without fixing the types of x and y, HOLogic.mk_eq (Bound 0, Bound 1) gives an error, because it can't find the type of Bound terms. I was just thinking to create the mk_eq term first, then wrap it inside a mk_all and itself inside another mk_all. Is there a better way to go about this? Thanks a lot in advance. Steve

**References**:**[isabelle] Constructing terms in ML***From:*Steve Wong

- Previous by Date: [isabelle] Constructing terms in ML
- Next by Date: [isabelle] set quick_and_dirty mode when running Isabelle from the command line?
- Previous by Thread: [isabelle] Constructing terms in ML
- Next by Thread: [isabelle] set quick_and_dirty mode when running Isabelle from the command line?
- Cl-isabelle-users September 2011 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