# mathlibdocumentation

tactic.rewrite_search.explain

# Tools to extract valid Lean code from a path found by rewrite search. #

@[protected, instance]
def tactic.rewrite_search.dir_pair.inhabited (α : Type u) [a : inhabited α] :
structure tactic.rewrite_search.dir_pair (α : Type u) :
Type u
• l : α
• r : α

A dir_pair is a pair of items designed to be accessed according to dir, a "direction" defined in the expr_lens library.

Instances for tactic.rewrite_search.dir_pair

Get one side of the pair, picking the side according to the direction.

Equations

Set one side of the pair, picking the side according to the direction.

Equations

Convert the pair to a list of its elements.

Equations

Convert the pair to a readable string format.

Equations
@[protected, instance]
Equations
@[protected, instance]

A data structure for the result of a splice operation. obstructed: There was more of the addr to be added left, but we hit a rw contained: The added addr was already contained, and did not terminate at an existing rw new: The added addr terminated at an existing rw or we could create a new one for it

Instances for tactic.rewrite_search.using_conv.splice_result

Explain a list of rewrites using conv_x tactics.

Construct a list of rewrites from a proof unit.

meta def tactic.rewrite_search.proof_unit.explain (rs : list ) (explain_using_conv : bool) :

Construct an explanation string from a proof unit.

Trace a human-readable explanation in Lean code of a proof generated by rewrite search. Emit it as "Try this: <code>" with each successive line of code indented.