mathlib documentation

tactic.rewrite_all.basic

inductive side :

Type

L : side
R : side

@[instance]

def side.inhabited :

@[instance]

def side.decidable_eq :

decidable_eq side

def side.other (a : side) :

Equations

side.R.other = side.L
side.L.other = side.R

def side.to_string (a : side) :

Equations

side.R.to_string = "R"
side.L.to_string = "L"

@[instance]

def side.has_to_string :

has_to_string side

Equations

side.has_to_string = {to_string := side.to_string}

meta structure tactic.rewrite_all.cfg :

Type

to_rewrite_cfg : tactic.rewrite_cfg
try_simp : bool
discharger : tactic unit
simplifier : expr → tactic (expr × expr)

meta structure tactic.rewrite_all.tracked_rewrite :

Type

exp : expr
proof : tactic expr
addr : option (list side)

meta def tactic.rewrite_all.tracked_rewrite.eval (rw : tactic.rewrite_all.tracked_rewrite) :

tactic (expr × expr)

meta def tactic.rewrite_all.tracked_rewrite.replace_target (rw : tactic.rewrite_all.tracked_rewrite) :

meta def tactic.rewrite_all.tracked_rewrite.replace_target_lhs (rw : tactic.rewrite_all.tracked_rewrite) :

meta def tactic.rewrite_all.tracked_rewrite.replace_target_rhs (rw : tactic.rewrite_all.tracked_rewrite) :