Zulip Chat Archive

Stream: new members

Topic: Tracing goals in have and show


view this post on Zulip Brian Milnes (Dec 20 2020 at 20:39):

I can't see (in either emacs or vs) the goal stack when using have and show. It works well when within begin and end.
When I move to the next lemma, it does not show "no goal". Nor does it show no goal after the lemma. This makes it a bit
harder to learn Lean that it should be. Is this intentional or a bug?

view this post on Zulip Alex J. Best (Dec 20 2020 at 20:41):

Can you give some screenshots /examples of where your cursor is and what you'd like to see?

view this post on Zulip Alex J. Best (Dec 20 2020 at 20:41):

I got into the habit of typing , (comma space) after everything to see the no goals after the last line

view this post on Zulip Kevin Buzzard (Dec 20 2020 at 21:06):

Can you confirm that you're using the leanprover-community version of Lean rather than the very old official Lean 3.4.2?


Last updated: May 14 2021 at 06:16 UTC