iApply: Add sufficiently many [] spec patterns per default?
I find my self repeatedly writing iApply (foo with "[] [] []")
in lambdaRust proofs. Would it make sense to extend the automatic "adding a []
to the end of th spec pattern list" that iApply
does, such that it will add as many []
as are needed to get the job done? Essentially, iApply foo
would always succeed if the conclusion of foo matches the goal, and all assumptions will only get the persistent contect -- spec patterns are only needed if one wants to give more than that? IMHO that would also improve the general workflow of working with iApply
since I don't need to look up in advance how many items I need to put into the spec pattern, I can just iApply
and then see which of the goals I get need further resources.