mathlib3 documentation

tactic.converter.interactive

source
meta def old_conv.save_info (p : pos) :
old_conv unit
source
meta def old_conv.step {α : Type} (c : old_conv α) :
old_conv unit
source
meta def old_conv.istep {α : Type} (line0 col0 line col : ℕ) (c : old_conv α) :
old_conv unit
source
meta def old_conv.execute (c : old_conv unit) :
tactic unit
source
meta def old_conv.interactive.itactic  :
Type
source
meta def old_conv.interactive.whnf  :
old_conv unit
source
meta def old_conv.interactive.dsimp  :
old_conv unit
source
meta def old_conv.interactive.trace_state  :
old_conv unit
source
meta def old_conv.interactive.change (p : interactive.parse interactive.types.texpr) :
old_conv unit
source
meta def old_conv.interactive.find (p : interactive.parse (lean.parser.pexpr std.prec.max)) (c : old_conv.interactive.itactic) :
old_conv unit
source
meta def conv.replace_lhs (tac : expr → tactic (expr × expr)) :
conv unit
source
meta def conv.discharge_eq_lhs (tac : tactic unit) :
conv unit
source
@[protected]
meta def conv.interactive.conv (t : conv.interactive.itactic) :
conv unit

The conv tactic provides a conv within a conv. It allows the user to return to a previous state of the outer conv block to continue editing an expression without having to start a new conv block.

source
meta def conv.interactive.erw (q : interactive.parse tactic.interactive.rw_rules) (cfg : tactic.rewrite_cfg := {to_apply_cfg := {md := tactic.transparency.semireducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}, symm := bool.ff, occs := occurrences.all}) :
conv unit
source
meta def conv.interactive.guard_target (p : interactive.parse interactive.types.texpr) :
conv unit

guard_target t fails if the target of the conv goal is not t. We use this tactic for writing tests.

source
meta def tactic.interactive.old_conv (c : old_conv.interactive.itactic) :
tactic unit
source
meta def tactic.interactive.find (p : interactive.parse (lean.parser.pexpr std.prec.max)) (c : old_conv.interactive.itactic) :
tactic unit
source
meta def tactic.interactive.conv_lhs (loc : interactive.parse (optional (lean.parser.tk "at" *> lean.parser.ident))) (p : interactive.parse (optional (lean.parser.tk "in" *> (lean.parser.pexpr std.prec.max)))) (c : conv.interactive.itactic) :
tactic unit
source
meta def tactic.interactive.conv_rhs (loc : interactive.parse (optional (lean.parser.tk "at" *> lean.parser.ident))) (p : interactive.parse (optional (lean.parser.tk "in" *> (lean.parser.pexpr std.prec.max)))) (c : conv.interactive.itactic) :
tactic unit