When there are multiple goals and a tactic proves the first, it silently jumps to the next one. This confuses beginners about what happened in their proof.
Make it more visible that the subgoal has been completed and one moves to the next one. The classical example is induction n the jump from the base case to the induction step.
joneugster
commented
1 year ago
When there are multiple goals and a tactic proves the first, it silently jumps to the next one. This confuses beginners about what happened in their proof.
Make it more visible that the subgoal has been completed and one moves to the next one. The classical example is
induction nthe jump from the base case to the induction step.