mathlib documentation


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  :

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

meta def rsimp.repr_map  :

structure rsimp.config  :
  • attr_name : name
  • max_rounds :