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 that it is feasible to integrate the experiment with RedPRL.
The idea would be that we would expose the current version of the proof state in certain parts of the interface (such as in the interface for rules).
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 that it is feasible to integrate the experiment with RedPRL.
The idea would be that we would expose the current version of the proof state in certain parts of the interface (such as in the interface for rules).