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 :

tactic.transparency → expr → 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 :

tactic.transparency → name → bool → tactic hinst_lemma

source

meta constant hinst_lemma.pp :

hinst_lemma → tactic format

source

meta constant hinst_lemma.id :

hinst_lemma → name

source

@[protected, 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 :

hinst_lemmas → hinst_lemma → hinst_lemmas

source

meta constant hinst_lemmas.fold {α : Type} :

hinst_lemmas → α → (hinst_lemma → α → α) → α

source

meta constant hinst_lemmas.merge :

hinst_lemmas → hinst_lemmas → hinst_lemmas

source

meta def mk_hinst_singleton :

hinst_lemma → hinst_lemmas

source

meta def hinst_lemmas.pp (s : hinst_lemmas) :

tactic format

source

@[protected, 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) :

bool → list name → 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) :

list name → tactic unit

source

meta def merge_hinst_lemma_attrs (m : tactic.transparency) (as_simp : bool) :

list name → 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