mathlib3 documentation

tactic.rewrite_search.types

Types used in rewrite search. #

source
inductive tactic.rewrite_search.side  :
Type

side represents the side of an equation, either the left or the right.

Instances for tactic.rewrite_search.side
source
@[protected, instance]
def tactic.rewrite_search.side.inhabited  :
inhabited tactic.rewrite_search.side
source
@[protected, instance]
def tactic.rewrite_search.side.decidable_eq  :
decidable_eq tactic.rewrite_search.side
source
meta def tactic.rewrite_search.side.to_string  :
tactic.rewrite_search.side → format

Convert a side to a human-readable string.

source
def tactic.rewrite_search.side.to_xhs  :
tactic.rewrite_search.side → string

Convert a side to the string "lhs" or "rhs", for use in tactic name generation.

Equations
source
@[protected, instance]
meta def tactic.rewrite_search.side.has_to_format  :
has_to_format tactic.rewrite_search.side
source
meta structure tactic.rewrite_search.how  :
Type

A how contains information needed by the explainer to generate code for a rewrite. rule_index denotes which rule in the static list of rules is used. location describes which match of that rule was used, to work with nth_rewrite. addr is a list of "left" and "right" describing which subexpression is rewritten.

Instances for tactic.rewrite_search.how
source
meta def tactic.rewrite_search.how.to_string  :
tactic.rewrite_search.how → format

Convert a how to a human-readable string.

source
@[protected, instance]
meta def tactic.rewrite_search.how.has_to_format  :
has_to_format tactic.rewrite_search.how
source
meta structure tactic.rewrite_search.rewrite  :
Type

rewrite represents a single step of rewriting, that proves exp using proof.

source
meta structure tactic.rewrite_search.proof_unit  :
Type

proof_unit represents a sequence of steps that can be applied to one side of the equation to prove a particular expression.

source
meta structure tactic.rewrite_search.config  :
Type

Configuration options for a rewrite search. max_iterations controls how many vertices are expanded in the graph search. explain generates Lean code to replace the call to rewrite_search. explain_using_conv changes the nature of the explanation.