		Search-engine friendly clone of the ACL2 documentation.

ACL2-pc::induct

(atomic macro) generate subgoals using induction

Examples:
induct, (induct t)
   -- induct according to a heuristically-chosen scheme, creating
      a new subgoal for each base and induction step
(induct (append (reverse x) y))
   -- as above, but choose an induction scheme based on the term
      (append (reverse x) y) rather than on the current goal

General Form:
(induct &optional term)

Induct as in the corresponding :induct hint given to the theorem prover, creating new subgoals for the base and induction steps. If term is t or is not supplied, then use the current goal to determine the induction scheme; otherwise, use that term.

Remark: As usual, abbreviations are allowed in the term.

Remark: Induct actually calls the prove command with all processes turned off. Thus, you must be at top of the goal for an induct instruction.