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 tactic that would always fail. #35

Closed favonia closed 2 years ago

favonia commented 7 years ago

Maybe there is already one but I did not find it...

favonia commented 6 years ago

There is a great usage of this tactic---to mark completion. Right now RedPRL will accumulate unsolved subgoals along the way, and fail is a good way to make sure all the subgoals before a certain point are gone.