*To*: Steve Wong <s.wong.731 at gmail.com>*Subject*: Re: [isabelle] Better way to beta apply two terms*From*: Makarius <makarius at sketis.net>*Date*: Mon, 29 Aug 2011 14:32:13 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAFU+7wN=MWgAv=+mpMs9SjKWbG8DRNADAvERfNWDd-0otHWCwg@mail.gmail.com>*References*: <CAFU+7wN=MWgAv=+mpMs9SjKWbG8DRNADAvERfNWDd-0otHWCwg@mail.gmail.com>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Fri, 26 Aug 2011, Steve Wong wrote:

What is a better way to beta-apply two terms without using betapply, which can cause a type mismatch. For example: consts a :: nat F :: "'a => nat" ML {* val ftrm = @{term "F"}; val atrm = @{term "a"}; val res = betapply((ftrm,atrm)); type_of res *}The application succeeds, but the resulting term isn't well-typed (thustype_of fails). betapply doesn't seem to change the input type of F froma variable to "Nat.nat". Is there a better way of beta applying suchthat the input type can automatically be updated?

Makarius

**References**:**[isabelle] Better way to beta apply two terms***From:*Steve Wong

- Previous by Date: Re: [isabelle] Type unification failed
- Next by Date: Re: [isabelle] [isabelle-dev] Malformed YXML encoding
- Previous by Thread: [isabelle] Better way to beta apply two terms
- Next by Thread: [isabelle] Type unification failed
- Cl-isabelle-users August 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