IACL2 is an infix version of the ACL2
theorem proving system that performs I/O in infix
format. It is intended to make initial
experiments with ACL2 somewhat simpler for those unfamiliar with or
opposed to Lisp prefix syntax. (It is not an interface for experts, as
some of the more advanced aspects of ACL2 are not supported by the
infix parser.) Some examples of the syntax:
Function idiv (m : integer, n : integer | n ~~= 0)
{ ifix ( m/n ) };
/* Idiv takes two integer arguments, the second of which cannot = zero */
Theorem distributivity-of-minus-over-plus
{-(x + y) = -x + -y};
Theorem car-nth-0 { consp(x) -> x.car = x[0] };
