 which is nothing similar to a disease).</p>
<ul>
<li>a  <strong>lambda-abstraction</strong> <code>(λ [x T] e)</code> with <code>x</code> the name of the <strong>binding variable</strong>, <code>T</code> a term corresponding to the type of <code>x</code> and <code>e</code> a lambda-term called the <strong>body</strong> of the abstraction</li>
</ul>
<p>This is as we largely discussed the (single-argument) function constructor. In the concrete syntax, the most common notations are as follows:</p>
<pre><code 