mathlib documentation

core.init.meta.backward

source
meta constant tactic.back_lemmas  :
Type

source
meta constant tactic.mk_back_lemmas_core (a : tactic.transparency) :
tactic tactic.back_lemmas

source
meta constant tactic.back_lemmas_insert_core (a : tactic.transparency) (a_1 : tactic.back_lemmas) (a_2 : expr) :
tactic tactic.back_lemmas

source
meta constant tactic.back_lemmas_find (a : tactic.back_lemmas) (a_1 : expr) :
tactic (list expr)

source
meta def tactic.mk_back_lemmas  :
tactic tactic.back_lemmas

source
meta def tactic.back_lemmas_insert (a : tactic.back_lemmas) (a_1 : expr) :
tactic tactic.back_lemmas

source
meta constant tactic.backward_chaining_core (a : tactic.transparency) (a_1 : bool) (a_2 : ℕ) (a_3 a_4 : tactic unit) (a_5 : tactic.back_lemmas) :
tactic unit

source
meta def tactic.back_lemmas_add_extra (a : tactic.transparency) (a_1 : tactic.back_lemmas) (a_2 : 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 (a : list expr) :
tactic unit

source
meta def tactic.back_chaining_using_hs  :
tactic unit