mathlib3 documentation

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 α] :

inhabited (tactic.rewrite_search.dir_pair α)

structure tactic.rewrite_search.dir_pair (α : 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

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

def tactic.rewrite_search.dir_pair.set {α : Type} (p : tactic.rewrite_search.dir_pair α) :

expr_lens.dir → α → tactic.rewrite_search.dir_pair α

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

Equations

p.set expr_lens.dir.A v = {l := p.l, r := v}
p.set expr_lens.dir.F v = {l := v, r := p.r}

def tactic.rewrite_search.dir_pair.to_list {α : Type} (p : tactic.rewrite_search.dir_pair α) :

Convert the pair to a list of its elements.

Equations

p.to_list = [p.l, p.r]

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.

Equations

p.to_string = to_string p.l ++ "-" ++ to_string p.r

@[protected, instance]

def tactic.rewrite_search.dir_pair.has_to_string {α : Type} [has_to_string α] :

has_to_string (tactic.rewrite_search.dir_pair α)

Equations

tactic.rewrite_search.dir_pair.has_to_string = {to_string := tactic.rewrite_search.dir_pair.to_string _inst_1}

@[protected, instance]

def tactic.rewrite_search.using_conv.splice_result.inhabited :

inhabited tactic.rewrite_search.using_conv.splice_result

inductive tactic.rewrite_search.using_conv.splice_result :

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

meta def tactic.rewrite_search.using_conv.explain_rewrites (rs : list (expr × bool)) (s : tactic.rewrite_search.side) (hows : list tactic.rewrite_search.how) :

Explain a list of rewrites using conv_x tactics.

meta def tactic.rewrite_search.proof_unit.rewrites (u : tactic.rewrite_search.proof_unit) (rs : list (expr × bool)) :

list (expr × bool)

Construct a list of rewrites from a proof unit.

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

Construct an explanation string from a proof unit.

meta def tactic.rewrite_search.explain_search_result (cfg : tactic.rewrite_search.config) (rules : list (expr × bool)) (proof : expr) (units : list tactic.rewrite_search.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.