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
semicolon and tactic state display #201
Comments
Is it possible to display not just the first goal, but all goals? example : true ∧ true ∧ true :=
by split; split; trivial
-- ^ 1 goal:\n⊢ true
/- but I'd rather see: 2 goals:\n⊢ true\n⊢ true ∧ true -/
-- ^ 1 goal:\n⊢ true
/- but I'd rather see: 2 goals:\n⊢ true\n⊢ true -/ |
The problem is that your gloss is not true - there are not 2 goals after the first tactic, there is one goal and the second tactic is read twice. The wording What I would rather see is
where the two responses mean that lean has responded twice to a |
The advantage of this approach is that you can more easily follow what happens in complex tactic blocks that are being evaluated multiple times by |
Thanks Mario, that makes better sense. |
A related bug report (possibly caused by #239?): In the following example, the tactic before any tactic involving import order.lattice
variables {α : Type*} [lattice α] {x y z : α}
example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
begin
apply le_antisymm, -- cursor here shows 1 goal
apply le_inf; sorry,
end |
I wish we could see how the tactic state changes before and after semicolons.
I asked Mario about this in this Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/semicolon.20and.20tactic.20state
Apparently this requires changes to the global parser?
The text was updated successfully, but these errors were encountered: