structure smt_pre_config :
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.
structure smt_config :
- cc_cfg : cc_config
- em_cfg : ematch_config
- pre_cfg : smt_pre_config
- em_attr : name
Configuration for the smt_state object.
- em_attr: is the attribute name for the hinst_lemmas that are used for ematching