mathlib documentation

tactic.rewrite_search.discovery

Generating a list of rewrites to use as steps in rewrite search. #

meta def tactic.rewrite_search.rewrite_search_attr :

(user_attribute unit)

Use this attribute to make rewrite_search use this definition during search.

meta def tactic.rewrite_search.collect_rules :

tactic (list (expr × bool))

Collect rewrite rules to use from the environment.

meta def tactic.rewrite_search.get_rewrites (rules : list (expr × bool)) (exp : expr) (cfg : tactic.rewrite_search.config) :

tactic (buffer tactic.rewrite_search.rewrite)

Get all rewrites that start at the given expression and use one of the given rewrite rules.