+ <title>Syntax</title>
+ <para>To describe syntax in this manual we use the following conventions:</para>
+ <orderedlist>
+ <listitem>Non terminal symbols are emphasized and have a link to their definition. E.g.: &term;</listitem>
+ <listitem>Terminal symbols are in bold. E.g.: <emphasis role="bold">theorem</emphasis></listitem>
+ <listitem>Optional sequences of elements are put in square brackets.
+ E.g.: [<emphasis role="bold">in</emphasis> &term;]</listitem>
+ <listitem>Alternatives are put in square brakets and they are separated
+ by vertical bars. E.g.: [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>]</listitem>
+ <listitem>Repetition of sequences of elements are given by putting the
+ first sequence in square brackets, that are followed by three dots.
+ E.g.: [<emphasis role="bold">and</emphasis> &term;]…</listitem>
+ </orderedlist>
+ <sect1 id="terms_and_co">
+ <title>Terms & co.</title>
+ <sect2 id="lexical">
+ <title>Lexical conventions</title>
+ <table>
+ <tgroup cols="4">
+ <thead />
+ <tbody>
+ <row>
+ <entry id="id">&id;</entry>
+ <entry>::=</entry>
+ <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ <table>
+ <tgroup cols="4">
+ <thead />
+ <tbody>
+ <row>
+ <entry id="nat">&nat;</entry>
+ <entry>::=</entry>
+ <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ <table>
+ <tgroup cols="4">
+ <thead />
+ <tbody>
+ <row>
+ <entry id="uri">&uri;</entry>
+ <entry>::=</entry>
+ <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ </sect2>
+ <sect2 id="terms">
+ <title>Terms</title>
+ <table>
+ <tgroup cols="4">
+ <thead />
+ <tbody>
+ <row>
+ <entry id="term">&term;</entry>
+ <entry>::=</entry>
+ <entry>&sterm;</entry>
+ <entry>simple or delimited term</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry>&term; &term;</entry>
+ <entry>application</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">λ</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
+ <entry>λ-abstraction</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">Π</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
+ <entry>dependent product meant to define a datatype</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">∀</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
+ <entry>dependent product meant to define a proposition</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
+ <entry>non-dependent product (logical implication or function space)</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">let</emphasis> [&id;|(&id;<emphasis role="bold">:</emphasis> &term;)] <emphasis role="bold">≝</emphasis> &term; <emphasis role="bold">in</emphasis> &term;</entry>
+ <entry>local definition</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">let</emphasis>
+ [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
+ &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
+ [<emphasis role="bold">:</emphasis> &term;]
+ <emphasis role="bold">≝</emphasis> &term;
+ </entry>
+ <entry>(co)recursive definitions</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry/>
+ <entry>
+ [<emphasis role="bold">and</emphasis>
+ [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
+ [<emphasis role="bold">:</emphasis> &term;]
+ <emphasis role="bold">≝</emphasis> &term;]…
+ </entry>
+ <entry/>
+ </row>
+ <row>
+ <entry/>
+ <entry/>
+ <entry>
+ <emphasis role="bold">in</emphasis> &term;
+ </entry>
+ <entry/>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry>…</entry>
+ <entry>user provided notation</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>