Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

suffices: multiple goals not appearing as the text suggests? #82

Open
dijkstracula opened this issue Oct 23, 2023 · 0 comments
Open

suffices: multiple goals not appearing as the text suggests? #82

dijkstracula opened this issue Oct 23, 2023 · 0 comments

Comments

@dijkstracula
Copy link
Contributor

Dear all,

In Propositions and Proofs, when the suffices keyword is introduced, the text reads, "Writing suffices hq : q leaves us with two goals.". I was expecting, in the style of using Coq, to see those two goals explicitly shown in the context window/infoview. However, the incomplete example does not do so: there is still only one goal, and it appears to be unchanged from the previous line.

variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  have hp : p := h.left
  suffices hq : q
Expected type

pq: Prop
h: p ∧ q
⊢ q ∧ p

Is there a different infoview that I should be using that the text doesn't explicitly call out? Or, has this behaviour since changed?

Version

#eval Lean.versionString: 4.0.0, commit 96de208a6b1a575b3f07d978965573d5b6fad454

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant