*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Unable to generate code for ?P = (%x. True)*From*: Duraid Madina <duraid at kinoko.c.u-tokyo.ac.jp>*Date*: Tue, 4 Nov 2008 01:43:48 +0900*User-agent*: Mutt/1.4.2.1i

I was expecting a bool from the following, but instead got the error in the subject: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ theory odd imports Primes begin definition m_cond :: "nat => (nat => nat) => bool" where "m_cond n mf = ((ALL i. i <= n --> 0 < mf i) & (ALL i j. i <= n & j <= n & i ~= j --> gcd (mf i, mf j) = 1))" value "m_cond 1 (%x. 3)" ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Am I doing something evil here? Duraid

**Follow-Ups**:**Re: [isabelle] Unable to generate code for ?P = (%x. True)***From:*Tobias Nipkow

**Re: [isabelle] Unable to generate code for ?P = (%x. True)***From:*Tobias Nipkow

- Previous by Date: [isabelle] Using different symbols in LaTeX
- Next by Date: Re: [isabelle] Unable to generate code for ?P = (%x. True)
- Previous by Thread: [isabelle] Using different symbols in LaTeX
- Next by Thread: Re: [isabelle] Unable to generate code for ?P = (%x. True)
- Cl-isabelle-users November 2008 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