mathlib documentation

core.init.meta.smt.rsimp

source
meta def mk_hinst_lemma_attr_from_simp_attr (attr_decl_name attr_name simp_attr_name ex_attr_name : name) :
tactic unit

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.

source
meta def no_rsimp  :
(user_attribute name_set)

source
meta def rsimp_attr  :
(user_attribute hinst_lemmas)

source
meta def rsimp.is_value_like (a : expr) :
bool

source
meta def rsimp.explicit_size (a : expr) :
tactic ℕ

Return the size of term by considering only explicit arguments.

source
meta def rsimp.choose (ccs : cc_state) (e : expr) :
tactic expr

Choose smallest element (with respect to explicit_size) in es equivalence class.

source
meta def rsimp.repr_map  :
Type

source
meta def rsimp.mk_repr_map  :
expr_map expr

source
meta def rsimp.to_repr_map (ccs : cc_state) :
tactic rsimp.repr_map

source
meta def rsimp.rsimplify (ccs : cc_state) (e : expr) (m : option rsimp.repr_map := none) :
tactic (expr × expr)

source
structure rsimp.config  :
Type
  • attr_name : name
  • max_rounds : ℕ

source
meta def rsimp.collect_implied_eqs (cfg : rsimp.config := {attr_name := name.mk_string "rsimp_attr" name.anonymous, max_rounds := 8}) (extra : hinst_lemmas := hinst_lemmas.mk) :
tactic cc_state

source
meta def rsimp.rsimplify_goal (ccs : cc_state) (m : option rsimp.repr_map := none) :
tactic unit

source
meta def rsimp.rsimplify_at (ccs : cc_state) (h : expr) (m : option rsimp.repr_map := none) :
tactic unit

source
meta def tactic.rsimp (cfg : rsimp.config := {attr_name := name.mk_string "rsimp_attr" name.anonymous, max_rounds := 8}) (extra : hinst_lemmas := hinst_lemmas.mk) :
tactic unit

source
meta def tactic.rsimp_at (h : expr) (cfg : rsimp.config := {attr_name := name.mk_string "rsimp_attr" name.anonymous, max_rounds := 8}) (extra : hinst_lemmas := hinst_lemmas.mk) :
tactic unit

source
meta def tactic.interactive.rsimp  :
tactic unit