*To*: <stark at cs.stonybrook.edu>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Mysterious behavior of "let"*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 26 Sep 2016 08:44:47 +0200*In-reply-to*: <b55551dc-4088-1a89-e1d4-413f50e74d7e@starkeffect.com>*References*: <b55551dc-4088-1a89-e1d4-413f50e74d7e@starkeffect.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

Hi Eugene,

Best, Andreas On 25/09/16 12:43, Eugene W. Stark wrote:

Can somebody explain this mysterious behavior? Thanks. - Gene Stark ---------------------- theory Barf imports Main begin lemma shows nothing proof - let ?x0 = 100 let ?x1 = 101 let ?y = "\<lambda>i. if i = 0 then ?x0 else ?x1" have "?y 0 = ?x0" by presburger let ?x = 102 have "?y 0 = ?x0" oops (* ?x0 is now 102 *) end

**References**:**[isabelle] Mysterious behavior of "let"***From:*Eugene W. Stark

- Previous by Date: [isabelle] Mysterious behavior of "let"
- Next by Date: [isabelle] Mutual coinduction
- Previous by Thread: [isabelle] Mysterious behavior of "let"
- Next by Thread: [isabelle] Mutual coinduction
- Cl-isabelle-users September 2016 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