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.
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 Stringfield toJudgement, and modifying?andUnsolvedGoalsto properly print these labels.As an aside, the printing of
?andUnsolvedGoalscould probably be unified in some way.