mathlib documentation

core.init.meta.smt.ematch

source
meta constant hinst_lemma  :
Type

Heuristic instantiation lemma

source
meta constant hinst_lemmas  :
Type

source
meta constant hinst_lemma.mk_core (a : tactic.transparency) (a_1 : expr) (a_2 : bool) :
tactic hinst_lemma

mk_core m e as_simp, m is used to decide which definitions will be unfolded in patterns. If as_simp is tt, then this tactic will try to use the left-hand-side of the conclusion as a pattern.

source
meta constant hinst_lemma.mk_from_decl_core (a : tactic.transparency) (a_1 : name) (a_2 : bool) :
tactic hinst_lemma

source
meta constant hinst_lemma.pp (a : hinst_lemma) :
tactic format

source
meta constant hinst_lemma.id (a : hinst_lemma) :
name

source
@[instance]
meta def hinst_lemma.has_to_tactic_format  :
has_to_tactic_format hinst_lemma

source
meta def hinst_lemma.mk (h : expr) :
tactic hinst_lemma

source
meta def hinst_lemma.mk_from_decl (h : name) :
tactic hinst_lemma

source
meta constant hinst_lemmas.mk  :
hinst_lemmas

source
meta constant hinst_lemmas.add (a : hinst_lemmas) (a_1 : hinst_lemma) :
hinst_lemmas

source
meta constant hinst_lemmas.fold {α : Type} (a : hinst_lemmas) (a_1 : α) (a_2 : hinst_lemma → α → α) :
α

source
meta constant hinst_lemmas.merge (a a_1 : hinst_lemmas) :
hinst_lemmas

source
meta def mk_hinst_singleton (a : hinst_lemma) :
hinst_lemmas

source
meta def hinst_lemmas.pp (s : hinst_lemmas) :
tactic format

source
@[instance]
meta def hinst_lemmas.has_to_tactic_format  :
has_to_tactic_format hinst_lemmas

source
meta def to_hinst_lemmas_core (m : tactic.transparency) (a : bool) (a_1 : list name) (a_2 : hinst_lemmas) :
tactic hinst_lemmas

source
meta def mk_hinst_lemma_attr_core (attr_name : name) (as_simp : bool) :
tactic unit

source
meta def mk_hinst_lemma_attrs_core (as_simp : bool) (a : list name) :
tactic unit

source
meta def merge_hinst_lemma_attrs (m : tactic.transparency) (as_simp : bool) (a : list name) (a_1 : hinst_lemmas) :
tactic hinst_lemmas

source
meta def mk_hinst_lemma_attr_set (attr_name : name) (attr_names simp_attr_names : list name) :
tactic unit

Create a new "cached" attribute (attr_name : user_attribute hinst_lemmas). It also creates "cached" attributes for each attr_names and simp_attr_names if they have not been defined yet. Moreover, the hinst_lemmas for attr_name will be the union of the lemmas tagged with attr_name, attrs_name, and simp_attr_names. For the ones in simp_attr_names, we use the left-hand-side of the conclusion as the pattern.

source
meta def get_hinst_lemmas_for_attr (attr_name : name) :
tactic hinst_lemmas

source
structure ematch_config  :
Type
  • max_instances : ℕ
  • max_generation : ℕ

source
meta constant ematch_state  :
Type

source
meta constant ematch_state.mk (a : ematch_config) :
ematch_state

source
meta constant ematch_state.internalize (a : ematch_state) (a_1 : expr) :
tactic ematch_state

source
meta constant tactic.ematch_core (a : tactic.transparency) (a_1 : cc_state) (a_2 : ematch_state) (a_3 : hinst_lemma) (a_4 : expr) :
tactic (list (expr × expr) × cc_state × ematch_state)

source
meta constant tactic.ematch_all_core (a : tactic.transparency) (a_1 : cc_state) (a_2 : ematch_state) (a_3 : hinst_lemma) (a_4 : bool) :
tactic (list (expr × expr) × cc_state × ematch_state)

source
meta def tactic.ematch (a : cc_state) (a_1 : ematch_state) (a_2 : hinst_lemma) (a_3 : expr) :
tactic (list (expr × expr) × cc_state × ematch_state)

source
meta def tactic.ematch_all (a : cc_state) (a_1 : ematch_state) (a_2 : hinst_lemma) (a_3 : bool) :
tactic (list (expr × expr) × cc_state × ematch_state)