mathlib3 documentation

core / init.meta.smt.ematch

source
meta constant hinst_lemma  :
Type

Heuristic instantiation lemma

Instances for hinst_lemma
source
meta constant hinst_lemmas  :
Type
Instances for hinst_lemmas
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
  • max_instances : ℕ
  • max_generation : ℕ
Instances for ematch_config

Ematching

source
meta constant ematch_state  :
Type
source
meta constant ematch_state.mk  :
ematch_config → ematch_state
source
meta constant ematch_state.internalize  :
ematch_state → expr → tactic ematch_state
source
meta constant tactic.ematch_core  :
tactic.transparency → cc_state → ematch_state → hinst_lemma → expr → tactic (list (expr × expr) × cc_state × ematch_state)
source
meta constant tactic.ematch_all_core  :
tactic.transparency → cc_state → ematch_state → hinst_lemma → bool → tactic (list (expr × expr) × cc_state × ematch_state)
source
meta def tactic.ematch  :
cc_state → ematch_state → hinst_lemma → expr → tactic (list (expr × expr) × cc_state × ematch_state)
source
meta def tactic.ematch_all  :
cc_state → ematch_state → hinst_lemma → bool → tactic (list (expr × expr) × cc_state × ematch_state)