mathlib documentation

core.init.meta.converter.interactive

meta def conv.save_info  :

meta def conv.step {α : Type} :
conv αconv unit

meta def conv.istep {α : Type} :
conv αconv unit

meta def conv.execute  :

meta def conv.solve1  :

meta def conv.interactive.itactic  :
Type