sml-redprl
sml-redprl copied to clipboard
RedPRL
The People's Refinement Logic
Coercion of V types in RedPRL is currently wrong because the algorithm does not work in the open-term setting.
These are exactly the case that our direct computation rules cannot deal with (because it is not a stable reduction). Also, @favonia, what happens with HITs? do we generate typed...
The trailing tactics in `[t1, t2, t3, ..., tn]` will not run if the number of subgoals is less then the number of tactics, and that should generate a warning.
The metalanguage has some very dope stuff, that I'd like to start explaining (as a basis for continuing to develop it and improve it, and eventually expose it to the...
In what real-life situations we will have >10 variables in a context? See #239.
Top-level things don't have source locations; we need to add source locations to the metalanguage operations. A simple example is that `Print Foo.` will result in: ``` [Unknown Location] [Error]:...
I want a function similar to what we call "normal" in cubicaltt. The purpose of this function is to normalize/simplify terms as far as possible, this means that it has...
