search

RedPRL / sml-dependent-lcf

A library for the next generation of LCF refiners, with support for dependent refinement—Long Live the Anti-Realist Struggle!
16 stars 1 forks source link

Is it a bug or a feature that `each`/`thenl` don't check for equal list lengths #19

Closed wilcoxjay closed 7 years ago

wilcoxjay commented 7 years ago

Based on experience with other LCF implementations, I would expect to get an error when providing the wrong number of tactics for the current number of goals. Is this intentional?

jonsterling commented 7 years ago

@wilcoxjay Good question; in my previous implementations of LCF, I think that I went with the traditional choice of raising an error in these cases. I think that is more "technically correct" in some sense...

However, I have found that in practice, it is much nicer to be able to write scripts that are a bit less sensitive than this; for instance, it is nice to say t; [t1, t2] rather than t; [t1, t2, id, id , id, id, id]. In a refiner, usually rules are arranged such that the "most important" goals appear first, and all the silly wellformedness subgoals that you hope can be discharged automatically eventually get put at the end, so this works nicely in practice.

It could be reasonable to have both the versions that require the correct length and those which do not, if there is demand for it...

wilcoxjay commented 7 years ago

Sounds good, thanks!