Tools to extract valid Lean code from a path found by rewrite search. #
@[protected, instance]
- 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
- tactic.rewrite_search.dir_pair.has_sizeof_inst
- tactic.rewrite_search.dir_pair.inhabited
- tactic.rewrite_search.dir_pair.has_to_string
def
tactic.rewrite_search.dir_pair.get
{α : Type}
(p : tactic.rewrite_search.dir_pair α) :
expr_lens.dir → α
Get one side of the pair, picking the side according to the direction.
Equations
- p.get expr_lens.dir.A = p.r
- p.get expr_lens.dir.F = p.l
Set one side of the pair, picking the side according to the direction.
def
tactic.rewrite_search.dir_pair.to_list
{α : Type}
(p : tactic.rewrite_search.dir_pair α) :
list α
Convert the pair to a list of its elements.
def
tactic.rewrite_search.dir_pair.to_string
{α : Type}
[has_to_string α]
(p : tactic.rewrite_search.dir_pair α) :
Convert the pair to a readable string format.
@[protected, instance]
Equations
@[protected, instance]
- 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
Instances for tactic.rewrite_search.using_conv.splice_result
- tactic.rewrite_search.using_conv.splice_result.has_sizeof_inst
- tactic.rewrite_search.using_conv.splice_result.inhabited