mathlib documentation


Types used in rewrite search. #

inductive tactic.rewrite_search.side  :

side represents the side of an equation, either the left or the right.

Convert a side to a human-readable string.

Convert a side to the string "lhs" or "rhs", for use in tactic name generation.

meta structure  :

A 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 nth_rewrite. addr is a list of "left" and "right" describing which subexpression is rewritten.

Convert a how to a human-readable string.

meta structure tactic.rewrite_search.rewrite  :

rewrite represents a single step of rewriting, that proves exp using proof.

meta structure tactic.rewrite_search.proof_unit  :

proof_unit represents a sequence of steps that can be applied to one side of the equation to prove a particular expression.

meta structure tactic.rewrite_search.config  :

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 rewrite_search. explain_using_conv changes the nature of the explanation.