<varlistentry>
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">check</emphasis> &term;</para>
+ <para><emphasis role="bold">check</emphasis> &sterm;</para>
</listitem>
</varlistentry>
<varlistentry>
</variablelist>
</para>
</sect1>
+ <!--
<sect1 id="command_eval">
<title>eval</title>
<para><userinput>eval red on t</userinput></para>
</variablelist>
</para>
</sect1>
+ -->
+ <!--
<sect1 id="command_prefer_coercion">
<title>prefer coercion</title>
<para><userinput>prefer coercion u</userinput></para>
</variablelist>
</para>
</sect1>
+ -->
<sect1 id="command_coercion">
<title>coercion</title>
- <para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
+ <para><userinput>coercion nocomposites c : ty ≝ u on s : S to T</userinput></para>
<para>
<variablelist>
<varlistentry>
<listitem>
<para>
<emphasis role="bold">coercion</emphasis>
- (&uri; | &term; <emphasis role="bold">with</emphasis>)
- [ &nat; [&nat;]]
- [ <emphasis role="bold">nocomposites</emphasis> ]
+ [ <emphasis role="bold">nocomposites</emphasis> ] &id;
+ [ : &term; <emphasis role="bold">≝</emphasis> &term;
+ <emphasis role="bold">on</emphasis>
+ &id; : &term;
+ <emphasis role="bold">to</emphasis> &term; ]
</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>Declares <command>u</command> as an implicit coercion.
- If the type of <command>u</command> is
- <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command> the coercion target is
- <command>T(n - ariety)</command> while its source is
- <command>T(n - ariety - saturation - 1)</command>.
- Every time a term <command>x</command>
- of type source is used with expected type target, Matita
+ <para>Declares <command>c</command> as an implicit coercion.
+ If only <command>c</command> is given, <command>u</command>
+ is the constant named by <command>c</command>,
+ <command>ty</command> its declared type,
+ <command>s</command> the name of the last variable abstracted in
+ in <command>ty</command>, <command>S</command> the type of
+ this last variable and <command>T</command> the target of
+ <command>ty</command>. The user can specify all these component to
+ have full control on how the coercion is indexed.
+ The type of the body of the coercion <command>u</command> must be
+ convertible to the declared one <command>ty</command>. Let it be
+ <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command>.
+ Then <command>s</command> must be one of <command>x1</command> …
+ <command>xn</command> (possibly prefixed by <command>_</command>
+ if the product is non dependent). Let <command>s</command>
+ be <command>xi</command> in the following.
+ Then <command>S</command> must be <command>Ti</command>
+ where all bound variables are replaced by <command>?</command>,
+ and <command>T</command> must be <command>Tn</command>
+ where all bound variable are replaced by <command>?</command>.
+ For example the following command
+ declares a coercions from vectors of any length to lists of
+ natural numbers.</para>
+
+ <para><userinput>coercion nocomposites v2l : ∀n:nat.∀v:Vect nat n.
+ List nat ≝ l_of_v on _v : Vect nat ? to List nat</userinput></para>
+
+
+ <para>Every time a term <command>x</command>
+ of a type that matches <command>S</command>
+ (<command>Vect nat ?</command> here)
+ is used with an expected
+ type that matches <command>T</command>
+ (<command>List nat</command> here), Matita
automatically replaces <command>x</command> with
- <command>(u ? … ? x ? … ?)</command> to avoid a typing error.</para>
- Note that the number of <command>?</command> added after
- <command>x</command> is saturation.
+ <command>(u ? … ? x ? … ?)</command> to avoid a typing error.
+ Note that the position of <command>x</command> is determined by
+ <command>s</command>.</para>
+
<para>Implicit coercions are not displayed to the user:
<command>(u ? … ? x)</command> is rendered simply
as <command>x</command>.</para>
+
<para>When a coercion <command>u</command> is declared
from source <command>s</command> to target <command>t</command>
and there is already a coercion <command>u'</command> of
a composite implicit coercion is automatically computed
by Matita unless <emphasis role="bold">nocomposites</emphasis>
is specified.</para>
+
+ <para>Note that <command>Vect nat ?</command> can be replaced with
+ <command>Vect ? ?</command> to index the coercion is a loose way.</para>
</listitem>
</varlistentry>
</variablelist>
</para>
</sect1>
+ <!--
<sect1 id="command_default">
<title>default</title>
<para><userinput>default "s" u<subscript>1</subscript> … u<subscript>n</subscript></userinput></para>
</variablelist>
</para>
</sect1>
+ -->
+ <!--
<sect1 id="command_hint">
<title>hint</title>
<para><userinput>hint</userinput></para>
</variablelist>
</para>
</sect1>
+ -->
<sect1 id="command_include">
<title>include</title>
<para><userinput>include "s"</userinput></para>
<link linkend="interpretation">interpretation</link> that was active
when the file <command>s</command> was compiled last time
is made active. The same happens for declarations of
- <link linkend="command_default">default definitions and
- theorems</link> and disambiguation
+ <!-- <link linkend="command_default">default definitions and
+ theorems</link> and --> disambiguation
hints (<link linkend="command_alias">aliases</link>).
On the contrary, theorem and definitions declared in a file can be
immediately used without including it.</para>
- <para>The file <command>s</command> is automatically compiled
- if it is not compiled yet.
+ <para>The file <command>s</command> is automatically compiled
+ if it is not compiled yet.
+ </para>
+ <para>
+ If the file <command>s</command> was already included, either
+ directly or recursively, the commands does nothing.
</para>
</listitem>
</varlistentry>
</variablelist>
</para>
</sect1>
+ <sect1 id="command_include_alias">
+ <title>include alias</title>
+ <para><userinput>include alias "s"</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">include</emphasis> <emphasis role="bold">alias</emphasis> &qstring;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Every
+ <link linkend="interpretation">interpretation</link>
+ declared in the file <command>s</command> is re-declared
+ so to make it the preferred choice for disambiguation.
+ </para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <!--
<sect1 id="command_include_first">
<title>include' "s"</title>
<para><userinput></userinput></para>
</variablelist>
</para>
</sect1>
+ -->
+ <!--
<sect1 id="command_whelp">
<title>whelp</title>
<para><userinput>whelp locate "s"</userinput></para>
</variablelist>
</para>
</sect1>
+ -->
<sect1 id="command_qed">
<title>qed</title>
<para><userinput>qed</userinput></para>
</variablelist>
</para>
</sect1>
+ <sect1 id="command_qed_minus">
+ <title>qed-</title>
+ <para><userinput>qed-</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">qed-</emphasis>
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Saves the current interactive theorem or
+ definition without indexing. Therefore automation will ignore
+ it.
+ In order to do this, the set of sequents still to be proved
+ must be empty.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="command_unification_hint">
+ <title>unification hint</title>
+ <para><userinput>unification hint n ≔ v1 : T1,… vi : Ti; h1 ≟ t1, … hn ≟ tn ⊢ tl ≡ tr.</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Synopsis:</term>
+ <listitem>
+ <para>
+ <emphasis role="bold">unification hint</emphasis>
+ &nat;
+ <emphasis role="bold">≔</emphasis>
+ [ &id; [ <emphasis role="bold">:</emphasis> &term; ] ,.. ]
+ <emphasis role="bold">;</emphasis>
+ [ &id; <emphasis role="bold">≟</emphasis> &term; ,.. ]
+ <emphasis role="bold">⊢</emphasis>
+ &term; <emphasis role="bold">≡</emphasis> &term;
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Declares the hint at precedence <command>n</command></para>
+ <para>The file <command>hints_declaration.ma</command> must be
+ included to declare hints with that syntax.</para>
+ <para>Unification hints are described in the paper
+ "Hints in unification" by
+ Asperti, Ricciotti, Sacerdoti and Tassi.
+ </para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="command_universe_constraints">
+ <title>universe constraint</title>
+ <para>TODO</para>
+ <!--
+ <para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Synopsis:</term>
+ <listitem>
+ <para>
+ <emphasis role="bold">coercion</emphasis>
+ (&uri; | &term; <emphasis role="bold">with</emphasis>)
+ [ &nat; [&nat;]]
+ [ <emphasis role="bold">nocomposites</emphasis> ]
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Declares <command>u</command> as an implicit coercion.
+ If the type of <command>u</command> is
+ <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command> the coercion target is
+ <command>T(n - ariety)</command> while its source is
+ <command>T(n - ariety - saturation - 1)</command>.
+ Every time a term <command>x</command>
+ of type source is used with expected type target, Matita
+ automatically replaces <command>x</command> with
+ <command>(u ? … ? x ? … ?)</command> to avoid a typing error.</para>
+ Note that the number of <command>?</command> added after
+ <command>x</command> is saturation.
+ <para>Implicit coercions are not displayed to the user:
+ <command>(u ? … ? x)</command> is rendered simply
+ as <command>x</command>.</para>
+ <para>When a coercion <command>u</command> is declared
+ from source <command>s</command> to target <command>t</command>
+ and there is already a coercion <command>u'</command> of
+ target <command>s</command> or source <command>t</command>,
+ a composite implicit coercion is automatically computed
+ by Matita unless <emphasis role="bold">nocomposites</emphasis>
+ is specified.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ -->
+ </sect1>
+ <!--
<sect1 id="command_inline">
<title>inline</title>
<para><userinput>inline "s" params</userinput></para>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">definition</emphasis></entry>
+ <entry><emphasis role="bold"> definition</emphasis></entry>
<entry>Try give a <link linkend="definition">definition</link> flavour
</entry>
</row>
</table>
</sect2>
</sect1>
+ -->
</chapter>
projects / helm.git / blobdiff