*To*: "Hibou57 (Hibou57)" <yannick_duchene at yahoo.fr>*Subject*: Re: [isabelle] Infinitely recursive lambda expression or not?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sat, 14 Dec 2013 12:24:49 +0000*Cc*: John Wickerson <johnwickerson at cantab.net>, "cl-isabelle-users at lists.cam.ac.uk List" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <op.w720faa1esn74s@cardamome>*References*: <op.w72usxweule2fv@cardamome> <C743CBFE-029F-4E49-9A56-3695338394B8@cantab.net> <op.w720faa1esn74s@cardamome>

On 14 Dec 2013, at 12:17, Yannick <yannick_duchene at yahoo.fr> wrote: > Why is f(False) not False ? If it's built with False only and only disjunctions, where could True comes from? > > Or else may be my interpretation is wrong: I see it as an infinite sequence like “x ∨ x ∨ x ∨ x ∨ x ∨ …”. I’m afraid that’s your mistake. Such expressions simply don’t make sense. Larry Paulson

**Follow-Ups**:**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**References**:**[isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*John Wickerson

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick

- Previous by Date: Re: [isabelle] Infinitely recursive lambda expression or not?
- Next by Date: Re: [isabelle] Hide all constructors of a datatype automatically
- Previous by Thread: Re: [isabelle] Infinitely recursive lambda expression or not?
- Next by Thread: Re: [isabelle] Infinitely recursive lambda expression or not?
- Cl-isabelle-users December 2013 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