Attempting to factor out generic judgment (#11) from RedPRL into this library. It's going to be gnarly, because of the way that we deal with metavariables in ABTs; but at least, maybe we can hide it in this library until we give metavariables a locative treatment.
Very WIP. Will require further changes after I determine what is broken by integrating with RedPRL.
Attempting to factor out generic judgment (#11) from RedPRL into this library. It's going to be gnarly, because of the way that we deal with metavariables in ABTs; but at least, maybe we can hide it in this library until we give metavariables a locative treatment.
Very WIP. Will require further changes after I determine what is broken by integrating with RedPRL.