to be as faithful as possible to the theory and also to avoid working with low-level terms directly (they are somewhat unreadable even for the trained mind). Thanksfully, LaTTe also provides a <em>parser</em> for higher-level terms, the ones manipulated by the users.</p>
<p>Some lambda-calculi are untyped, other ones make a clear distinction between terms on the one side, and types on the other side. This is <em>not</em> the case with λC, although some terms are types and others are not (of course !). We w