mathlib documentation

meta def conv.save_info (p : pos) :

meta def conv.step {α : Type} (c : conv α) :

meta def conv.istep {α : Type} (line0 col0 line col ast : ℕ) (c : conv α) :

meta def conv.execute (c : conv unit) :

meta def conv.solve1 (c : conv unit) :

meta def conv.interactive.itactic  :

meta def conv.interactive.skip  :

meta def conv.interactive.whnf  :

meta def conv.interactive.dsimp (no_dflt : interactive.parse interactive.types.only_flag) (es : interactive.parse tactic.simp_arg_list) (attr_names : interactive.parse interactive.types.with_ident_list) (cfg : tactic.dsimp_config := {md := reducible, max_steps := simp.default_max_steps, canonize_instances := tt, single_pass := ff, fail_if_unchanged := tt, eta := tt, zeta := tt, beta := tt, proj := tt, iota := tt, unfold_reducible := ff, memoize := tt}) :

meta def conv.interactive.trace_lhs  :

meta def conv.interactive.change (p : interactive.parse interactive.types.texpr) :

meta def conv.interactive.congr  :

meta def conv.interactive.funext  :

meta def conv.interactive.to_lhs  :

meta def conv.interactive.to_rhs  :

meta def conv.interactive.done  :

meta def conv.interactive.find (p : interactive.parse (lean.parser.pexpr std.prec.max)) (c : conv.interactive.itactic) :

meta def conv.interactive.for (p : interactive.parse (lean.parser.pexpr std.prec.max)) (occs : interactive.parse (interactive.types.list_of lean.parser.small_nat)) (c : conv.interactive.itactic) :

meta def conv.interactive.simp (no_dflt : interactive.parse interactive.types.only_flag) (hs : interactive.parse tactic.simp_arg_list) (attr_names : interactive.parse interactive.types.with_ident_list) (cfg : tactic.simp_config_ext := {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, iota_eqn := ff, constructor_eq := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt, trace_lemmas := ff}, discharger := tactic.failed unit}) :

meta def conv.interactive.guard_lhs (p : interactive.parse interactive.types.texpr) :

meta def conv.interactive.rewrite (q : interactive.parse tactic.interactive.rw_rules) (cfg : tactic.rewrite_cfg := {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, symm := ff, occs := occurrences.all}) :

meta def conv.interactive.rw (q : interactive.parse tactic.interactive.rw_rules) (cfg : tactic.rewrite_cfg := {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, symm := ff, occs := occurrences.all}) :

meta def tactic.interactive.conv (loc : interactive.parse (lean.parser.tk "at" *> lean.parser.ident)?) (p : interactive.parse (lean.parser.tk "in" *> (lean.parser.pexpr std.prec.max))?) (c : conv.interactive.itactic) :