Major Section: ACL2-BUILT-INS
(must-be-equal logic exec) evaluates to
logic in the ACL2
logic but evaluates to
exec in raw Lisp. The point is to be able to
write one definition to reason about logically but another for evaluation.
Please see mbe and see mbt for appropriate macros to use, rather than
must-be-equal directly, since it is easy to commute the arguments
must-be-equal by accident.
In essence, the guard for
(must-be-equal x y) is
(equal x y).
However, note that
must-be-equal is a macro:
(must-be-equal logic exec) expands to
(mbe1 exec logic), which
expands to a call of