You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Right now, the field tactic output nonzero side conditions in the form of a boolean conjunction [&& _ != 0, ... & _ != 0].
Ideally in order to produce a stable script, one should not rely on this exact shape, and prepare with have : _ != 0 statements before the call to the field tactic.
The ideal output of field would be individual subgoals of the shape _ != 0 instead.
E.g.
Lemma test x y : x != 0 -> y != 0 -> 1 / (x * y) = 1/x * 1/y.
Proof.
Fail by move=> xNZ yNZ; field.
by move=> xNZ yNZ; field; do ?[apply/andP; split].
Qed.
The text was updated successfully, but these errors were encountered:
Right now, the
field
tactic output nonzero side conditions in the form of a boolean conjunction[&& _ != 0, ... & _ != 0]
.Ideally in order to produce a stable script, one should not rely on this exact shape, and prepare with
have : _ != 0
statements before the call to thefield
tactic.The ideal output of field would be individual subgoals of the shape
_ != 0
instead.E.g.
The text was updated successfully, but these errors were encountered: