TOTBWF/tactic-haskell

Optional Subgoal Labels

TOTBWF opened this issue · 0 comments

Sometimes, it helps to be able to label the subgoals, especially when handling inductive types like Bool.
Implementation-wise, this is as easy as adding a Maybe String field to Judgement, and modifying
? and UnsolvedGoals to properly print these labels.

As an aside, the printing of ? and UnsolvedGoals could probably be unified in some way.