+ <sect2 id="definition">
+ <title><emphasis role="bold">definition</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
+ <titleabbrev>definition</titleabbrev>
+ <para><userinput>definition f: T ≝ t</userinput></para>
+ <para><command>f</command> is defined as <command>t</command>;
+ <command>T</command> is its type. An error is raised if the type of
+ <command>t</command> is not convertible to <command>T</command>.</para>
+ <para><command>T</command> is inferred from <command>t</command> if
+ omitted.</para>
+ <para><command>t</command> can be omitted only if <command>T</command> is
+ given. In this case Matita enters in interactive mode and
+ <command>f</command> must be defined by means of tactics.</para>
+ <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
+ </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;]…]…
+</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>
+ <para>Declares a family of two mutually inductive types
+ <command>i</command> and <command>i'</command> whose types are
+ <command>S</command> and <command>S'</command>, which must be convertible
+ to sorts.</para>
+ <para>The constructors <command>ki</command> of type <command>Ti</command>
+ and <command>ki'</command> of type <command>Ti'</command> are also
+ simultaneously declared. The declared types <command>i</command> and
+ <command>i'</command> may occur in the types of the constructors, but
+ only in strongly positive positions according to the rules of the
+ calculus.</para>
+ <para>The whole family is parameterized over the arguments <command>x,y,z</command>.</para>
+ <para>If the keyword <command>coinductive</command> is used, the declared
+ types are considered mutually coinductive.</para>
+ <para>Elimination principles for the record are automatically generated
+ by Matita, if allowed by the typing rules of the calculus according to
+ the sort <command>S</command>. If generated,
+ they are named <command>i_ind</command>, <command>i_rec</command> and
+ <command>i_rect</command> according to the sort of their induction
+ predicate.</para>
+ </sect2>
+ <sect2 id="record">
+ <title><emphasis role="bold">record</emphasis> &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis><emphasis role="bold">{</emphasis>[&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:></emphasis>] &term;] [<emphasis role="bold">;</emphasis>&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:></emphasis>] &term;]…<emphasis role="bold">}</emphasis></title>
+ <titleabbrev>record</titleabbrev>
+ <para><userinput>record id x y z: S ≝ { f1: T1; …; fn:Tn }</userinput></para>
+ <para>Declares a new record family <command>id</command> parameterized over
+ <command>x,y,z</command>.</para>
+ <para><command>S</command> is the type of the record
+ and it must be convertible to a sort.</para>
+ <para>Each field <command>fi</command> is declared by giving its type
+ <command>Ti</command>. A record without any field is admitted.</para>
+ <para>Elimination principles for the record are automatically generated
+ by Matita, if allowed by the typing rules of the calculus according to
+ the sort <command>S</command>. If generated,
+ they are named <command>i_ind</command>, <command>i_rec</command> and
+ <command>i_rect</command> according to the sort of their induction
+ predicate.</para>
+ <para>For each field <command>fi</command> a record projection
+ <command>fi</command> is also automatically generated if projection
+ is allowed by the typing rules of the calculus according to the
+ sort <command>S</command>, the type <command>T1</command> and
+ the definability of depending record projections.</para>
+ <para>If the type of a field is declared with <command>:></command>,
+ the corresponding record projection becomes an implicit coercion.
+ This is just syntactic sugar and it has the same effect of declaring the
+ record projection as a coercion later on.</para>
+ </sect2>
+ </sect1>
+
+ <sect1 id="proofs">
+ <title>Proofs</title>
+ <sect2 id="theorem">
+ <title><emphasis role="bold">theorem</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
+ <titleabbrev>theorem</titleabbrev>
+ <para><userinput>theorem f: P ≝ p</userinput></para>
+ <para>Proves a new theorem <command>f</command> whose thesis is
+ <command>P</command>.</para>
+ <para>If <command>p</command> is provided, it must be a proof term for
+ <command>P</command>. Otherwise an interactive proof is started.</para>
+ <para><command>P</command> can be omitted only if the proof is not
+ interactive.</para>
+ <para>Proving a theorem already proved in the library is an error.
+ To provide an alternative name and proof for the same theorem, use
+ <command>variant f: P ≝ p</command>.</para>
+ <para>A warning is raised if the name of the theorem cannot be obtained
+ by mangling the name of the constants in its thesis.</para>
+ <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
+ </sect2>
+ <sect2 id="variant">
+ <title><emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
+ <titleabbrev>variant</titleabbrev>
+ <para><userinput>variant f: T ≝ t</userinput></para>
+ <para>Same as <command>theorem f: T ≝ t</command>, but it does not
+ complain if the theorem has already been proved. To be used to give
+ an alternative name or proof to a theorem.</para>
+ </sect2>
+ <sect2 id="lemma">
+ <title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
+ <titleabbrev>lemma</titleabbrev>
+ <para><userinput>lemma f: T ≝ t</userinput></para>
+ <para>Same as <command>theorem f: T ≝ t</command></para>
+ </sect2>
+ <sect2 id="fact">
+ <title><emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
+ <titleabbrev>fact</titleabbrev>
+ <para><userinput>fact f: T ≝ t</userinput></para>
+ <para>Same as <command>theorem f: T ≝ t</command></para>
+ </sect2>
+ <sect2 id="remark">
+ <title><emphasis role="bold">remark</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
+ <titleabbrev>remark</titleabbrev>
+ <para><userinput>remark f: T ≝ t</userinput></para>
+ <para>Same as <command>theorem f: T ≝ t</command></para>
+ </sect2>
+ </sect1>
+
+ <sect1 id="tacticargs">
+ <title>Tactic arguments</title>
+ <para>This section documents the syntax of some recurring arguments for
+ tactics.</para>
+
+ <sect2 id="introsspec">
+ <title>intros-spec</title>
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>intros-spec</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.intros-spec">&intros-spec;</entry>
+ <entry>::=</entry>
+ <entry>[&nat;] [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ <para>The natural number is the number of new hypotheses to be introduced. The list of identifiers gives the name for the first hypotheses.</para>
+ </sect2>
+
+ <sect2 id="pattern">
+ <title>pattern</title>
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>pattern</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.pattern">&pattern;</entry>
+ <entry>::=</entry>
+ <entry>&TODO;</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ <para>&TODO;</para>
+ </sect2>
+
+ <sect2 id="reduction-kind">
+ <title>reduction-kind</title>
+ <para>Reduction kinds are normalization functions that transform a term
+ to a convertible but simpler one. Each reduction kind can be used both
+ as a tactic argument and as a stand-alone tactic.</para>
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>reduction-kind</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.reduction-kind">&reduction-kind;</entry>
+ <entry>::=</entry>
+ <entry><emphasis role="bold">demodulate</emphasis></entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">normalize</emphasis></entry>
+ <entry>Computes the βδιζ-normal form</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">reduce</emphasis></entry>
+ <entry>Computes the βδιζ-normal form</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">simplify</emphasis></entry>
+ <entry>Computes a form supposed to be simpler</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">unfold</emphasis> [&sterm;]</entry>
+ <entry>δ-reduces the constant or variable if specified, or that
+ in head position</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">whd</emphasis></entry>
+ <entry>Computes the βδιζ-weak-head normal form</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ </sect2>
+ </sect1>