mathlib documentation

core / init.meta.smt.interactive

meta def smt_tactic.step {α : Type} (tac : smt_tactic α) :
meta def smt_tactic.istep {α : Type} (line0 col0 line col ast : ) (tac : smt_tactic α) :

Try to close main goal by using equalities implied by the congruence closure module.

Produce new facts using heuristic lemma instantiation based on E-matching. This tactic tries to match patterns from lemmas in the main goal with terms in the main goal. The set of lemmas is populated with theorems tagged with the attribute specified at smt_config.em_attr, and lemmas added using tactics such as smt_tactic.add_lemmas. The current set of lemmas can be retrieved using the tactic smt_tactic.get_lemmas.

Try the given tactic, and do nothing if it fails.

Keep applying the given tactic until it fails.

Apply the given tactic to all remaining goals.

Keep applying heuristic instantiation until the current goal is solved, or it fails.

Keep applying heuristic instantiation using the given lemmas until the current goal is solved, or it fails.