[isabelle] Unable to generate code for ?P = (%x. True)



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.