mathlib documentation

core / init.meta.backward

source
meta constant tactic.back_lemmas  :
Type
source
meta constant tactic.mk_back_lemmas_core  :
tactic.transparency → tactic tactic.back_lemmas
source
meta constant tactic.back_lemmas_insert_core  :
tactic.transparency → tactic.back_lemmas → expr → tactic tactic.back_lemmas
source
meta constant tactic.back_lemmas_find  :
tactic.back_lemmas → expr → tactic (list expr)
source
meta def tactic.mk_back_lemmas  :
tactic tactic.back_lemmas
source
meta def tactic.back_lemmas_insert  :
tactic.back_lemmas → expr → tactic tactic.back_lemmas
source
meta constant tactic.backward_chaining_core  :
tactic.transparency → bool → ℕ → tactic unit → tactic unit → tactic.back_lemmas → tactic unit
source
meta def tactic.back_lemmas_add_extra  :
tactic.transparency → tactic.back_lemmas → list expr → tactic tactic.back_lemmas
source
meta def tactic.back_chaining_core (pre_tactic leaf_tactic : tactic unit) (extra_lemmas : list expr) :
tactic unit
source
meta def tactic.back_chaining  :
tactic unit
source
meta def tactic.back_chaining_using  :
list expr → tactic unit
source
meta def tactic.back_chaining_using_hs  :
tactic unit