Generating a list of rewrites to use as steps in rewrite search. #
Use this attribute to make rewrite_search
use this definition during search.
def
tactic.rewrite_search.get_rewrites
(rules : list (expr × bool))
(exp : expr)
(cfg : tactic.rewrite_search.config) :
Get all rewrites that start at the given expression and use one of the given rewrite rules.