Types used in rewrite search. #
how contains information needed by the explainer to generate code for a rewrite.
rule_index denotes which rule in the static list of rules is used.
location describes which match of that rule was used, to work with
addr is a list of "left" and "right" describing which subexpression is rewritten.
Configuration options for a rewrite search.
max_iterations controls how many vertices are expanded in the graph search.
explain generates Lean code to replace the call to
explain_using_conv changes the nature of the explanation.