The transformation from BCI-nf to their types
The number of internal nodes in the type of a BCI-nf term is the same as the number of internal nodes in the BCI-nf term.
- For each lambda-node, draw an arc from its leaf, through the lambda-node, and to its child.
-
For each apply-node, draw an arc from its right child, through its left child, and to the apply-node.