Sorry reporting should pick up term mode sorries as well.

leanprover-community / repl

A simple REPL for Lean 4, returning information about errors and sorries.

54 stars 13 forks source link

Open semorrison opened 1 year ago

semorrison commented 1 year ago

We will need to do further inspection of the InfoTrees to find these, but shouldn't be hard.