Configuration for the smt tactic preprocessor. The preprocessor is applied whenever a new hypothesis is introduced.
simp_attr: is the attribute name for the simplification lemmas that are used during the preprocessing step.
max_steps: it is the maximum number of steps performed by the simplifier.
zeta: if tt, then zeta reduction (i.e., unfolding let-expressions) is used during preprocessing.
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
The current set of lemmas can be retrieved using the tactic
Remark: the given predicate is applied to every new instance. The instance is only added to the state if the predicate returns tt.