ACL2-pc::then
(macro)
apply one instruction to current goal and another to new subgoals
Example:
(then induct prove)
General Form:
(then first-instruction &optional completion must-succeed-flg)
Run first-instruction, and then run completion (another
instruction) on each subgoal created by first-instruction. If
must-succeed-flg is supplied and not nil, then halt at the first
``failure'' and remove the effects of the invocation of completion that
``failed''.
The default for completion is reduce.
