This PR is an experiment at using a new representation of values, Problem, to describe unification problems with a mixed prefix. Existentials are represented as binders in terms, and solving will eliminate them, resulting in a problem that can e.g. be translated directly into a Value.
This PR is an experiment at using a new representation of values,
Problem, to describe unification problems with a mixed prefix. Existentials are represented as binders in terms, and solving will eliminate them, resulting in a problem that can e.g. be translated directly into aValue.