Zulip Chat Archive

Stream: general

Topic: Missing goals in infoview when using `;`

Eric Wieser (Feb 03 2021 at 10:51):


example (a b : ) : a = a  b = b :=
  split,  -- two goals: `a = a`, `b = b`
  apply id,  -- one goal `a = a`
  refl; apply id, -- one goal `b = b`
  refl; apply id,

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