+ <production id="grammar.term">
+ <lhs>&term;</lhs>
+ <rhs>&sterm;</rhs>
+ <lineannotation></lineannotation>
+ </production>
+ </productionset>
+ -->
+
+ <para>
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>Terms</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.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>
+ &rec_def;
+ </entry>
+ <entry>(co)recursive definitions</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry/>
+ <entry>
+ [<emphasis role="bold">and</emphasis> &rec_def;]…
+ </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>
+ <row>
+ <entry id="grammar.rec_def">&rec_def;</entry>
+ <entry>::=</entry>
+ <entry>
+ &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
+ </entry>
+ <entry />
+ </row>
+ <row>
+ <entry />
+ <entry />
+ <entry>
+ [<emphasis role="bold">on</emphasis> &nat;]
+ [<emphasis role="bold">:</emphasis> &term;]
+ <emphasis role="bold">≝</emphasis> &term;]
+ </entry>
+ <entry />
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>Simple terms</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.sterm">&sterm;</entry>
+ <entry>::=</entry>
+ <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
+ <entry/>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry>&id;[<emphasis role="bold">\subst[</emphasis>
+ &id;<emphasis role="bold">≔</emphasis>&term;
+ [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">≔</emphasis>&term;]…
+ <emphasis role="bold">]</emphasis>]
+ </entry>
+ <entry>identifier with optional explicit named substitution</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry>&uri;</entry>
+ <entry>a qualified reference</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">Prop</emphasis></entry>
+ <entry>the impredicative sort of propositions</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">Set</emphasis></entry>
+ <entry>the impredicate sort of datatypes</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">Type</emphasis></entry>
+ <entry>one predicative sort of datatypes</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">?</emphasis></entry>
+ <entry>implicit argument</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">?n</emphasis>
+ [<emphasis role="bold">[</emphasis>
+ [<emphasis role="bold">_</emphasis>|&term;]…
+ <emphasis role="bold">]</emphasis>]</entry>
+ <entry>metavariable</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">match</emphasis> &term;
+ [ <emphasis role="bold">in</emphasis> &term; ]
+ [ <emphasis role="bold">return</emphasis> &term; ]
+ <emphasis role="bold">with</emphasis>
+ </entry>
+ <entry>case analysis</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry/>
+ <entry>
+ <emphasis role="bold">[</emphasis>
+ &match_branch;[<emphasis role="bold">|</emphasis>&match_branch;]…
+ <emphasis role="bold">]</emphasis>
+ </entry>
+ <entry/>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
+ <entry>cast</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry>…</entry>
+ <entry>user provided notation at precedence 90</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>Arguments</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.args">&args;</entry>
+ <entry>::=</entry>
+ <entry>
+ <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
+ </entry>
+ <entry>ignored argument</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry>
+ <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
+ </entry>
+ <entry>ignored argument</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
+ <entry></entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
+ <entry/>
+ </row>
+ <row>
+ <entry id="grammar.args2">&args2;</entry>
+ <entry>::=</entry>
+ <entry>&id;</entry>
+ <entry/>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…<emphasis role="bold">:</emphasis> &term;<emphasis role="bold">)</emphasis></entry>
+ <entry/>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>Pattern matching</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.match_branch">&match_branch;</entry>
+ <entry>::=</entry>
+ <entry>&match_pattern; <emphasis role="bold">⇒</emphasis> &term;</entry>
+ <entry />
+ </row>
+ <row>
+ <entry id="grammar.match_pattern">&match_pattern;</entry>
+ <entry>::=</entry>
+ <entry>&id;</entry>
+ <entry>0-ary constructor</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
+ <entry>n-ary constructor (binds the n arguments)</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ </para>