mathlib3 documentation

core / init.meta.smt.interactive

source
meta def smt_tactic.save_info (p : pos) :
smt_tactic unit
source
meta def smt_tactic.skip  :
smt_tactic unit
source
meta def smt_tactic.solve_goals  :
smt_tactic unit
source
meta def smt_tactic.step {α : Type} (tac : smt_tactic α) :
smt_tactic unit
source
meta def smt_tactic.istep {α : Type} (line0 col0 line col ast : ℕ) (tac : smt_tactic α) :
smt_tactic unit
source
meta def smt_tactic.execute (tac : smt_tactic unit) :
tactic unit
source
meta def smt_tactic.execute_with (cfg : smt_config) (tac : smt_tactic unit) :
tactic unit
source
@[protected, instance]
meta def smt_tactic.interactive.executor  :
interactive.executor smt_tactic
source
meta def smt_tactic.interactive.itactic  :
Type
source
meta def smt_tactic.interactive.intros  :
interactive.parse (lean.parser.many lean.parser.ident) → smt_tactic unit
source
meta def smt_tactic.interactive.close  :
smt_tactic unit

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

source
meta def smt_tactic.interactive.ematch  :
smt_tactic unit

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.

source
meta def smt_tactic.interactive.apply (q : interactive.parse interactive.types.texpr) :
smt_tactic unit
source
meta def smt_tactic.interactive.fapply (q : interactive.parse interactive.types.texpr) :
smt_tactic unit
source
meta def smt_tactic.interactive.apply_instance  :
smt_tactic unit
source
meta def smt_tactic.interactive.change (q : interactive.parse interactive.types.texpr) :
smt_tactic unit
source
meta def smt_tactic.interactive.exact (q : interactive.parse interactive.types.texpr) :
smt_tactic unit
source
meta def smt_tactic.interactive.from (q : interactive.parse interactive.types.texpr) :
smt_tactic unit
source
meta def smt_tactic.interactive.assume  :
interactive.parse (sum.inl <$> (lean.parser.tk ":" *> interactive.types.texpr) <|> sum.inr <$> interactive.parse_binders interactive.types.tac_rbp) → tactic unit
source
meta def smt_tactic.interactive.have (h : interactive.parse (optional lean.parser.ident)) (q₁ : interactive.parse (optional (lean.parser.tk ":" *> interactive.types.texpr))) (q₂ : interactive.parse (optional (lean.parser.tk ":=" *> interactive.types.texpr))) :
smt_tactic unit
source
meta def smt_tactic.interactive.let (h : interactive.parse (optional lean.parser.ident)) (q₁ : interactive.parse (optional (lean.parser.tk ":" *> interactive.types.texpr))) (q₂ : interactive.parse (optional (lean.parser.tk ":=" *> interactive.types.texpr))) :
smt_tactic unit
source
meta def smt_tactic.interactive.add_fact (q : interactive.parse interactive.types.texpr) :
smt_tactic unit
source
meta def smt_tactic.interactive.trace_state  :
smt_tactic unit
source
meta def smt_tactic.interactive.trace {α : Type} [has_to_tactic_format α] (a : α) :
smt_tactic unit
source
meta def smt_tactic.interactive.destruct (q : interactive.parse interactive.types.texpr) :
smt_tactic unit
source
meta def smt_tactic.interactive.by_cases (q : interactive.parse interactive.types.texpr) :
smt_tactic unit
source
meta def smt_tactic.interactive.by_contradiction  :
smt_tactic unit
source
meta def smt_tactic.interactive.by_contra  :
smt_tactic unit
source
meta def smt_tactic.interactive.add_lemma (l : interactive.parse interactive.types.pexpr_list_or_texpr) :
smt_tactic unit
source
meta def smt_tactic.interactive.add_lhs_lemma (l : interactive.parse interactive.types.pexpr_list_or_texpr) :
smt_tactic unit
source
meta def smt_tactic.interactive.add_eqn_lemmas_for (ids : interactive.parse (lean.parser.many lean.parser.ident)) :
smt_tactic unit
source
meta def smt_tactic.interactive.add_eqn_lemmas (ids : interactive.parse (lean.parser.many lean.parser.ident)) :
smt_tactic unit
source
meta def smt_tactic.interactive.ematch_using (l : interactive.parse interactive.types.pexpr_list_or_texpr) :
smt_tactic unit
source
meta def smt_tactic.interactive.try (t : smt_tactic.interactive.itactic) :
smt_tactic unit

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

source
meta def smt_tactic.interactive.iterate (t : smt_tactic.interactive.itactic) :
smt_tactic unit

Keep applying the given tactic until it fails.

source
meta def smt_tactic.interactive.all_goals (t : smt_tactic.interactive.itactic) :
smt_tactic unit

Apply the given tactic to all remaining goals.

source
meta def smt_tactic.interactive.induction (p : interactive.parse tactic.interactive.cases_arg_p) (rec_name : interactive.parse interactive.types.using_ident) (ids : interactive.parse interactive.types.with_ident_list) (revert : interactive.parse (optional (lean.parser.tk "generalizing" *> lean.parser.many lean.parser.ident))) :
smt_tactic unit
source
meta def smt_tactic.interactive.simp (use_iota_eqn : interactive.parse (optional (lean.parser.tk "!"))) (no_dflt : interactive.parse interactive.types.only_flag) (hs : interactive.parse tactic.simp_arg_list) (attr_names : interactive.parse interactive.types.with_ident_list) (cfg : tactic.simp_config_ext := {to_simp_config := {max_steps := simp.default_max_steps, contextual := bool.ff, lift_eq := bool.tt, canonize_instances := bool.tt, canonize_proofs := bool.ff, use_axioms := bool.tt, zeta := bool.tt, beta := bool.tt, eta := bool.tt, proj := bool.tt, iota := bool.tt, iota_eqn := bool.ff, constructor_eq := bool.tt, single_pass := bool.ff, fail_if_unchanged := bool.tt, memoize := bool.tt, trace_lemmas := bool.ff}, discharger := tactic.failed unit}) :
smt_tactic unit

Simplify the target type of the main goal.

source
meta def smt_tactic.interactive.dsimp (no_dflt : interactive.parse interactive.types.only_flag) (es : interactive.parse tactic.simp_arg_list) (attr_names : interactive.parse interactive.types.with_ident_list) :
smt_tactic unit
source
meta def smt_tactic.interactive.rsimp  :
smt_tactic unit
source
meta def smt_tactic.interactive.add_simp_lemmas  :
smt_tactic unit
source
meta def smt_tactic.interactive.eblast  :
smt_tactic unit

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

source
meta def smt_tactic.interactive.eblast_using (l : interactive.parse interactive.types.pexpr_list_or_texpr) :
smt_tactic unit

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

source
meta def smt_tactic.interactive.guard_expr_eq (t : expr) (p : interactive.parse (lean.parser.tk ":=" *> interactive.types.texpr)) :
smt_tactic unit
source
meta def smt_tactic.interactive.guard_target (p : interactive.parse interactive.types.texpr) :
smt_tactic unit