Optional Subgoal Labels
TOTBWF opened this issue · 0 comments
TOTBWF commented
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.