sml-dependent-lcf
sml-dependent-lcf copied to clipboard
Consider getting rid of backtracking
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.