If our occur check succeeds, we get back the checked tree, but over the thickened set of variables. The ko (`knockout') function allows us to exploit this value.

ko takes a variable w from a set, and a tree t over the set one smaller (ie thickened at w): exactly the kind of tree returned by check. It returns the substitution which replaces w by t and thickens all the other variables.

The combined effect of |>, ko and check is to implement the replacement of a variable by a tree which does not contain it. Not only is the variable replaced: it is removed from the set available, and this removal is reflected in the type of ko.

Tidiness suggests that we should prove a wrapped-up version of thickElim called koElim. Can you guess what it says? (Hint, useful properties 1 and 2.)

Next: unification as optimisation | Prev: apply ind hyps | Up: contents