		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::wrap-induct

(atomic macro) same as induct, but create a single goal

Examples:
wrap-induct
(wrap-induct t)
(wrap-induct (append (reverse x) y))

General Form:
(wrap-induct &optional term)

The wrap-induct command is identical to the interactive proof-builder's induct command (see ACL2-pc::induct), except that only a single goal is created: the conjunction of the base and induction steps.

Note: The output will generally indicate that more than goal has been created, e.g.:

Creating two new goals:  (MAIN . 1) and (MAIN . 2).

However, wrap-induct always creates a unique goal (when it succeeds). A subsequent message clarifies this, for example:

NOTE: Created ONLY one new goal, which is the current goal:
  (MAIN . 1)