check does for tree what thick does for fin. It tries to compress the variable space of a tree by throwing out variable w. Of course, it can't do this if w occurs in the tree.

The green versions of leaf and ^ are the obvious `exception handling' versions of their red constructor counterparts. In this text, I'll call the green versions !leaf and !^ The `else' clause is nothing special: I'm too lazy to write the other three lines.

I apologise profusely to any readers who are red-green colourblind, and thus subjected to further overloading. I hope it isn't too confusing.

Next: check's elim rule | Prev: mapping the leaves | Up: contents