+ <table>
+ <tgroup>
+ <thead />
+ <tbody>
+ <row>
+ <entry id="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_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
+ [
+ <emphasis role="bold">|</emphasis>
+ &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
+ ]…<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>
+ <tgroup>
+ <thead />
+ <tbody>
+ <row>
+ <entry id="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>
+ </tbody>
+ </tgroup>
+ </table>
+
+ <table>
+ <tgroup>
+ <thead />
+ <tbody>
+ <row>
+ <entry id="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>