X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=6c9ad43af74097f740569d63d827fbf3424fbd96;hb=dca4170c5ce5f2cd6be8ae1dc0422bd6a680b43f;hp=7e22f33043d39ec5e0fcb62e7ce0c20ca1e41593;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git
diff --git a/matita/matita/help/C/sec_commands.xml b/matita/matita/help/C/sec_commands.xml
index 7e22f3304..6c9ad43af 100644
--- a/matita/matita/help/C/sec_commands.xml
+++ b/matita/matita/help/C/sec_commands.xml
@@ -60,7 +60,7 @@
Synopsis:
- check &term;
+ check &sterm;
@@ -74,6 +74,7 @@
+
+
coercion
- coercion u with ariety saturation nocomposites
+ coercion nocomposites c : ty â u on s : S to T
@@ -135,29 +139,60 @@
coercion
- (&uri; | &term; with)
- [ &nat; [&nat;]]
- [ nocomposites ]
+ [ nocomposites ] &id;
+ [ : &term; â &term;
+ on
+ &id; : &term;
+ to &term; ]
Action:
- Declares u as an implicit coercion.
- If the type of u is
- âx1:T1. ⦠âx(n-1):T(n-1).Tn the coercion target is
- T(n - ariety) while its source is
- T(n - ariety - saturation - 1).
- Every time a term x
- of type source is used with expected type target, Matita
+ Declares c as an implicit coercion.
+ If only c is given, u
+ is the constant named by c,
+ ty its declared type,
+ s the name of the last variable abstracted in
+ in ty, S the type of
+ this last variable and T the target of
+ ty. 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 u must be
+ convertible to the declared one ty. Let it be
+ âx1:T1. ⦠âx(n-1):T(n-1).Tn.
+ Then s must be one of x1 â¦
+ xn (possibly prefixed by _
+ if the product is non dependent). Let s
+ be xi in the following.
+ Then S must be Ti
+ where all bound variables are replaced by ?,
+ and T must be Tn
+ where all bound variable are replaced by ?.
+ For example the following command
+ declares a coercions from vectors of any length to lists of
+ natural numbers.
+
+ coercion nocomposites v2l : ân:nat.âv:Vect nat n.
+ List nat â l_of_v on _v : Vect nat ? to List nat
+
+
+ Every time a term x
+ of a type that matches S
+ (Vect nat ? here)
+ is used with an expected
+ type that matches T
+ (List nat here), Matita
automatically replaces x with
- (u ? ⦠? x ? ⦠?) to avoid a typing error.
- Note that the number of ? added after
- x is saturation.
+ (u ? ⦠? x ? ⦠?) to avoid a typing error.
+ Note that the position of x is determined by
+ s.
+
Implicit coercions are not displayed to the user:
(u ? ⦠? x) is rendered simply
as x.
+
When a coercion u is declared
from source s to target t
and there is already a coercion u' of
@@ -165,11 +200,15 @@
a composite implicit coercion is automatically computed
by Matita unless nocomposites
is specified.
+
+ Note that Vect nat ? can be replaced with
+ Vect ? ? to index the coercion is a loose way.
+
+
includeinclude "s"
@@ -315,14 +357,43 @@
hints (aliases).
On the contrary, theorem and definitions declared in a file can be
immediately used without including it.
- The file s is automatically compiled
- if it is not compiled yet.
+ The file s is automatically compiled
+ if it is not compiled yet.
+
+
+ If the file s was already included, either
+ directly or recursively, the commands does nothing.
+
+ include alias
+ include alias "s"
+
+
+
+ Synopsis:
+
+ includealias &qstring;
+
+
+
+ Action:
+
+ Every
+ interpretation
+ declared in the file s is re-declared
+ so to make it the preferred choice for disambiguation.
+
+
+
+
+
+
+
+
qedqed
@@ -401,7 +475,117 @@
+
+ qed-
+ qed-
+
+
+
+ Synopsis:
+
+ qed-
+
+
+
+
+ Action:
+
+ 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.
+
+
+
+
+
+
+ unification hint
+ unification hint n â v1 : T1,⦠vi : Ti; h1 â t1, ⦠hn â tn ⢠tl â¡ tr.
+
+
+
+ Synopsis:
+
+
+ unification hint
+ &nat;
+ â
+ [ &id; [ : &term; ] ,.. ]
+ ;
+ [ &id; â &term; ,.. ]
+ â¢
+ &term; â¡ &term;
+
+
+
+
+ Action:
+
+ Declares the hint at precedence n
+ The file hints_declaration.ma must be
+ included to declare hints with that syntax.
+ Unification hints are described in the paper
+ "Hints in unification" by
+ Asperti, Ricciotti, Sacerdoti and Tassi.
+
+
+
+
+
+ -->
+
+
+ universe constraint
+ TODO
+
+
+