| Interface Summary | |
|---|---|
| Node | Represents a node in a term DAG. |
| Substitution | The result of unification, either successful or not. |
| Term | A term node. |
| Var | A variable node. |
| Class Summary | |
|---|---|
| Substitution.Binding | |
| Unification | This is an implementation of the "near linear" algorithm for solving syntactic unification as described in the paper linked below.1 No recursive terms are allowed, meaning the "occurrs check" is performed on the input. |