Lines Matching defs:even
292 ; Problem 2a-1: Define the constant *even-program* as an M1 program that takes
294 ; is even and with 0 on the stack if i is odd. For example, if the program is
300 (defconst *even-program*
317 (defun even-sched (i)
323 (even-sched (- i 2))))))
325 (defun test-even (i)
328 (run (even-sched i)
332 *even-program*)))))
334 (defthm test-even-theorem
335 (and (equal (test-even 18) 1)
336 (equal (test-even 19) 0)
337 (equal (test-even 235) 0)
338 (equal (test-even 234) 1))