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.
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.
constant
tactic.ematch_core
:
tactic.transparency → cc_state → ematch_state → hinst_lemma → expr → tactic (list (expr × expr) × cc_state × ematch_state)
constant
tactic.ematch_all_core
:
tactic.transparency → cc_state → ematch_state → hinst_lemma → bool → tactic (list (expr × expr) × cc_state × ematch_state)
def
tactic.ematch
:
cc_state → ematch_state → hinst_lemma → expr → tactic (list (expr × expr) × cc_state × ematch_state)
def
tactic.ematch_all
:
cc_state → ematch_state → hinst_lemma → bool → tactic (list (expr × expr) × cc_state × ematch_state)