Eric Wieser (Feb 03 2021 at 10:51):
example (a b : ℕ) : a = a ∧ b = b := begin split, -- two goals: `a = a`, `b = b` apply id, -- one goal `a = a` refl; apply id, -- one goal `b = b` refl; apply id, end
Comments show the goal state at the end of each line, after the comma. If a line contains a
;, then the goal view at the end of the previous line is truncated to show just one goal.
Gabriel Ebner (Feb 03 2021 at 10:59):
Eric Wieser (Feb 03 2021 at 11:07):
Right, this is exactly the report in this comment: https://github.com/leanprover-community/lean/issues/201#issuecomment-654603146
Last updated: Aug 03 2023 at 10:10 UTC