General Recursion in Type Theory : Unification :
Proofs
Ana's thesis contains formal proofs of the following:
- unify is total, .e.g., all lists satisfy UniAcc.
- unify returns
Nothing only if the equations
aren't unifiable.
- The domain of the resulting substitution is a subset of the variables that
occur in the equations.
- The resulting substitution is idempotent.
- The resulting substitution is a most general unifier.