Tools to extract valid Lean code from a path found by rewrite search. #
Set one side of the pair, picking the side according to the direction.
- obstructed : tactic.rewrite_search.using_conv.splice_result
- contained : tactic.rewrite_search.using_conv.splice_result
- new : tactic.rewrite_search.using_conv.app_addr → tactic.rewrite_search.using_conv.splice_result
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
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.