sml-dependent-lcf
sml-dependent-lcf copied to clipboard
RedPRL
A library for the next generation of LCF refiners, with support for dependent refinement—Long Live the Anti-Realist Struggle!
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...
I want to try out alternative representations of the proof that that would avoid premature substitutions; but to do this, I need to somehow make the proof state abstract so...
The example demonstrates dependency, but in a silly / confusing way. Should replace this with something like a refiner for first order logic, or a little dependent type theory.