cooltt
cooltt copied to clipboard
Lightweight unification
I want to see if it is possible to make the nbe equality checker return a list of flex-flex and flex-rigid constraints which would make the equation true. Alternatively, a naive but possibly workable-to-start version would be to raise such a constraint as an exception which carries a continuation, kind of like an algebraic effect.