Our current debuggability of misbehaving tactics is extremely lacking. Instead we'd like to trace a rose tree of which tactics were run in each hole. My rough understanding of this is that we can stick it in the extract --- possibly using the new annotate combinator in refinery.
Our current debuggability of misbehaving tactics is extremely lacking. Instead we'd like to trace a rose tree of which tactics were run in each hole. My rough understanding of this is that we can stick it in the extract --- possibly using the new
annotatecombinator inrefinery.