tactic.rewrite_all.basic

source

inductive side :

Type

L : side
R : side

Instances for side

side.has_sizeof_inst
side.inhabited
side.has_to_string

source

@[protected, instance]

def side.inhabited :

inhabited side

source

@[protected, instance]

def side.decidable_eq :

decidable_eq side

source

def side.other :

side → side

Equations

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

source

def side.to_string :

side → string

Equations

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

source

@[protected, instance]

def side.has_to_string :

has_to_string side

Equations

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

source

meta structure tactic.rewrite_all.cfg :

Type

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

source

meta structure tactic.rewrite_all.tracked_rewrite :

Type

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

source

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

tactic (expr × expr)

source

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

tactic unit

source

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

tactic unit

source

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

tactic unit