mathlib documentation

core / init.meta.smt.ematch

meta constant hinst_lemma  :
Type

Heuristic instantiation lemma

meta constant hinst_lemmas  :
Type

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.

meta constant hinst_lemma.id  :
meta constant hinst_lemmas.mk  :
meta constant hinst_lemmas.fold {α : Type} :
hinst_lemmasα → (hinst_lemmaα → α) → α
meta def mk_hinst_lemma_attr_core (attr_name : name) (as_simp : bool) :
meta def mk_hinst_lemma_attrs_core (as_simp : bool) :
meta def mk_hinst_lemma_attr_set (attr_name : name) (attr_names simp_attr_names : list name) :

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.

structure ematch_config  :
Type
  • max_instances :
  • max_generation :
meta constant ematch_state  :
Type