Autotactics

The autotactics are used primarily for typechecking. Trivial

Does various steps of trivial reasoning, including
• NthHyp
• NthDecl
• Eq
• Contradiction - Both P and occur in hypothesis list.
• Concl is the term True or one of the hypotheses is either the term False or the term Void.

          Auto

Repeatedly tries the following until no further progress is made.
• Trivial
• GenExRepD
• MemCD for member and EqCD on reflexive equality conclusions. Only works on non-recursive primitive terms.
• Arith
• Arithmetic equality reasoning, in case concl is where a and b arithmetically simplify to same. (By arithmetically simplify, we mean simplify subterms which involve the basic arithmetic operators and rem.)
• If concl is or where T is subset of the integers, then open up T.

  SIAuto

Like Auto but also tries using the SupInf tactic.

Like Auto but uses the SupInf' tactic instead of the Arith tactic.

Auto and its variants frequently encounter the same goals over and over again, so