sml-dependent-lcf icon indicating copy to clipboard operation
sml-dependent-lcf copied to clipboard

Consider getting rid of backtracking

Open jonsterling opened this issue 7 years ago • 0 comments

We found that backtracking was basically useless in practice for RedPRL, because the state space would just blow up. I'm thinking that it actually may be a bad idea, and that in cases where we think we need backtracking, what we really need is to redesign the proof theory.

jonsterling avatar Feb 26 '18 12:02 jonsterling