Lines Matching defs:run
117 (defun run (sched s)
120 (run (cdr sched) (step s))))
153 (run
196 (equal (run
273 (run (ifact-sched n)
328 (run (even-sched i)
657 (run (repeat 0 1000)
673 (run (repeat 0 1000)
737 (defthm run-app
738 (equal (run (app a b) s)
739 (run b (run a s))))
741 (defthm run-opener
742 (and (equal (run nil s) s)
743 (equal (run (cons th sched) s)
744 (run sched (step s)))))
746 (in-theory (disable run))
784 ; will run this program to completion.
850 ; run this program to completion. We've already done this:
870 (run (ifact-sched n)
894 (equal (run (ifact-loop-sched n)
906 (equal (run (ifact-sched n)
916 ; We can now disable sched-ifact so that we never run the bytecode
933 (equal (run (ifact-sched n)
947 (run (ifact-sched n)
962 (run (ifact-sched n)
1143 'run))