lean
lean copied to clipboard
fix(init/meta/converter/interactive): Do not allow rw to create ⊢ goals in conv mode
This is an attempt at the approach described at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Closing.20.60.E2.8A.A2.60.20goals.20in.20.60conv.60.20mode/near/212702071
A contrived example where this applies:
import algebra.ring
variables {α : Type*} [ring α] {a b c : α}
lemma obvious : c = 1 → (a * b) * c = a * b := λ h, by {rw [h, mul_one]}
example (hc : c = 1) (hb : b = 1) : (a * b) * c = a := begin
conv_lhs {
rw obvious, -- this now fails, as it creates goals that can't be closed
-- TODO: allow a tactic block to be passed as a trailing argument
},
rw [hb, mul_one],
end
Could you add some tests showing the desired new behavior?
Where would you like the test to go? https://github.com/leanprover-community/lean/tree/master/tests/lean/interactive/conv.lean?
At any rate, this doesn't work yet, and I need help to make it work.
There are a few types of tests:
- Lean files in
tests/lean
should generate the corresponding.lean.expected.out
file. - Lean files in
tests/lean/run
should run without creating any output - Lean files in
tests/lean/fail
should fail
See also doc/fixing_tests.md
.