mathlib documentation

tactic.rewrite_search.explain

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

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.

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

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

Explain a list of rewrites using conv_x tactics.

Construct a list of rewrites from a proof unit.

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: " with each successive line of code indented.