sml-dependent-lcf
sml-dependent-lcf copied to clipboard
Published
20 hours ago •
RedPRL
RedPRL
A library for the next generation of LCF refiners, with support for dependent refinement—Long Live the Anti-Realist Struggle!
Results
3
sml-dependent-lcf issues
Sort by
recently updated
recently updated
newest added
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.