Open alexkeizer opened 2 years ago
The problem was that { $a:tactic; all_goals $b:tactic }
, with curly braces, was explicitly requiring it to close the goals. Removing them solved the problem.
We still want to focus the main goal, before applying a
, so that b
only works on those goals introduced by a
.
example {x y : Nat} : y = 0 ∨ y ≠ 0 :=
by
cases y;
cases x and_then {
apply Or.inl;
rfl
}
apply Or.inr
simp
Turns out focus
does exactly that, so the macro should be
macro a:tactic " and_then " b:tactic : tactic =>
`(tactic|
focus
$a:tactic; all_goals $b:tactic
)
I'd make a PR, but that seems a bit overkill for a change this tiny?
@alexkeizer the PR is highly welcome if you explain the change in the text. We're in the tactics chapter afterall 👍🏼
Page 60 suggests that
a and_then b
behaves the same asa <;> b
, but this is not the case whenb
does not close all goals;For example, if the second tactic is skip. The
<;>
version compiles just fine.But, the
and_then
version complains about unsolved goals.I don't readily see how to fix this while keeping it as a simple substitution-macro, but maybe this discrepancy should be pointed out in the text.