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

Add a function to apply a tactic to subgoals within a certain range #34

Closed favonia closed 6 years ago

favonia commented 7 years ago

This is to create an auto tactic that repeatedly applies the auto-step tactic in a certain range. So far these ranges are needed:

jonsterling commented 7 years ago

I keep forgetting to do this! I'm slammed today, but I will try to do it soon

favonia commented 7 years ago

Updated with what showed up in practice.

jonsterling commented 6 years ago

apply tac to everything before n can be achieved already using List.tabulate. But we need special support for the other one.