mathlib documentation

core / init.meta.converter.interactive

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  :
Type