mathlib documentation

core / init.meta.smt.rsimp

meta def mk_hinst_lemma_attr_from_simp_attr (attr_decl_name attr_name simp_attr_name ex_attr_name : name) :

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.

meta def rsimp.is_value_like  :
meta def rsimp.explicit_size  :

Return the size of term by considering only explicit arguments.

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

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

meta def rsimp.repr_map  :
Type
structure rsimp.config  :
Type
  • attr_name : name
  • max_rounds :