Create a rsimp attribute named attr_name, the attribute declaration is named attr_decl_name.
The cached hinst_lemmas structure is built using the lemmas marked with simp attribute simp_attr_name,
but not marked with ex_attr_name.
We say ex_attr_name is the "exception set". It is useful for excluding lemmas in simp_attr_name
which are not good or redundant for ematching.
Return the size of term by considering only explicit arguments.
def
rsimp.rsimplify
:
cc_state → expr → (option rsimp.repr_map := option.none) → tactic (expr × expr)
def
rsimp.collect_implied_eqs
:
(rsimp.config := {attr_name := name.mk_string "rsimp_attr" name.anonymous, max_rounds := 8}) → (hinst_lemmas := hinst_lemmas.mk) → tactic cc_state
def
tactic.rsimp
:
(rsimp.config := {attr_name := name.mk_string "rsimp_attr" name.anonymous, max_rounds := 8}) → (hinst_lemmas := hinst_lemmas.mk) → tactic unit
def
tactic.rsimp_at
:
expr → (rsimp.config := {attr_name := name.mk_string "rsimp_attr" name.anonymous, max_rounds := 8}) → (hinst_lemmas := hinst_lemmas.mk) → tactic unit