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 : ) (c : conv α) :

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

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

meta def conv.interactive.itactic  :
Type