sml-redprl
sml-redprl copied to clipboard
Warning about too many tactics in `[_, _, ..., _]`
The trailing tactics in [t1, t2, t3, ..., tn]
will not run if the number of subgoals is less then the number of tactics, and that should generate a warning.
@favonia I'm not sure if it really should generate a warning, because the shape of the proof state is dynamic. But I'm not strongly against it either...
I think it is confusing if part of the script is silently ignored. The warning will be generated dynamically. Maybe I misunderstood your concern? Are you worried about the tactic defined in the userland?
@favonia I guess I was thinking that one doesn't want a script to depend that sharply on the actual structure of the proof state, but now I think you're right and I was wrong.
With that said, what I think we do want to allow is to provide fewer tactics than needed; for instance [t1,t2]
should be fine, even if there are four subgoals. But we can make a warning if there are too many tactics provided.
Yes: being lazy is fine, but working too hard is a serious problem.