<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
+ <listitem><para>Non terminal symbols are emphasized and have a link to their
+ definition. E.g.: &term;</para></listitem>
+ <listitem><para>Terminal symbols are in bold. E.g.:
+ <emphasis role="bold">theorem</emphasis></para></listitem>
+ <listitem><para>Optional sequences of elements are put in square brackets.
+ E.g.: [<emphasis role="bold">in</emphasis> &term;]</para></listitem>
+ <listitem><para>Alternatives are put in square brakets and they are
+ separated by vertical bars. E.g.: [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>]</para></listitem>
+ <listitem><para>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>
+ E.g.: [<emphasis role="bold">and</emphasis> &term;]…</para></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>
+ <para>
+ <table frame="all" rowsep="0" colsep="0">
+ <title>id</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="id">&id;</entry>
+ <entry>::=</entry>
+ <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ <table frame="all" rowsep="0" colsep="0">
+ <title>nat</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="nat">&nat;</entry>
+ <entry>::=</entry>
+ <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ <table frame="all" rowsep="0" colsep="0">
+ <title>uri</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="uri">&uri;</entry>
+ <entry>::=</entry>
+ <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ </para>
</sect2>
<sect2 id="terms">
<title>Terms</title>
- <table>
+ <para>
+ <table frame="all" rowsep="0" colsep="0">
+ <title>Terms</title>
<tgroup cols="4">
- <thead />
<tbody>
<row>
<entry id="term">&term;</entry>
</tgroup>
</table>
- <table>
+ <table frame="all" rowsep="0" colsep="0">
+ <title>Simple terms</title>
<tgroup cols="4">
- <thead />
<tbody>
<row>
<entry id="sterm">&sterm;</entry>
</tgroup>
</table>
- <table>
+ <table frame="all" rowsep="0" colsep="0">
+ <title>Arguments</title>
<tgroup cols="4">
- <thead />
<tbody>
<row>
<entry id="args">&args;</entry>
</tgroup>
</table>
- <table>
+ <table frame="all" rowsep="0" colsep="0">
+ <title>Miscellaneous arguments</title>
<tgroup cols="4">
- <thead />
<tbody>
<row>
<entry id="args2">&args2;</entry>
</tgroup>
</table>
- <table>
+ <table frame="all" rowsep="0" colsep="0">
+ <title>Pattern matching</title>
<tgroup cols="4">
- <thead />
<tbody>
<row>
<entry id="match_pattern">&match_pattern;</entry>
</tbody>
</tgroup>
</table>
+ </para>
</sect2>
</sect1>
</sect2>
<sect2 id="inductive">
<title>[<emphasis role="bold">inductive</emphasis>|<emphasis role="bold">coinductive</emphasis>] &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…
-[<emphasis role="bold">with</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…]
+[<emphasis role="bold">with</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…]…
</title>
<titleabbrev>(co)inductive types declaration</titleabbrev>
<para><userinput>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</userinput></para>