X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=7e22f33043d39ec5e0fcb62e7ce0c20ca1e41593;hb=f4f44aa85f6d8ad07c44ce5890bd447f04b9c8a2;hp=1644c85bd88493728d926261f9b32211cb123a2c;hpb=c766ed6f754196fe55254d09189f1255054b95f1;p=helm.git
diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml
index 1644c85bd..7e22f3304 100644
--- a/helm/software/matita/help/C/sec_commands.xml
+++ b/helm/software/matita/help/C/sec_commands.xml
@@ -74,26 +74,87 @@
+
+ eval
+ eval red on t
+
+
+
+ Synopsis:
+
+ eval
+ &reduction-kind;
+ on
+ &term;
+
+
+
+ Action:
+
+ Opens a CIC browser window that shows
+ the reduct of
+ t
+ together with its type.
+
+
+
+
+
+
+ prefer coercion
+ prefer coercion u
+
+
+
+ Synopsis:
+
+
+ prefer coercion
+ (&uri; | &term;)
+
+
+
+
+ Action:
+
+ The already declared coercion u
+ is preferred to other coercions with the same source and target.
+
+
+
+
+
+ coercion
- coercion u
+ coercion u with ariety saturation nocompositesSynopsis:
- coercion &uri;
+
+ coercion
+ (&uri; | &term; with)
+ [ &nat; [&nat;]]
+ [ nocomposites ]
+ Action:
- Declares u as an implicit coercion
- from the type of its last argument (source)
- to its codomain (target). Every time a term x
+ 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
automatically replaces x with
- (u ? ⦠? x) to avoid a typing error.
+ (u ? ⦠? x ? ⦠?) to avoid a typing error.
+ Note that the number of ? added after
+ x is saturation.
Implicit coercions are not displayed to the user:
(u ? ⦠? x) is rendered simply
as x.
@@ -102,7 +163,8 @@
and there is already a coercion u' of
target s or source t,
a composite implicit coercion is automatically computed
- by Matita.
+ by Matita unless nocomposites
+ is specified.
@@ -148,6 +210,12 @@
expected object for 3rd URIexpected object for 4th URIexpected object for 5th URI
+ expected object for 6th URI
+ expected object for 7th URI
+ expected object for 8th URI
+ expected object for 9th URI
+ expected object for 10th URI
+ expected object for 11th URI
@@ -158,6 +226,12 @@
a theorem of type âA.âx,y,z:A.eq A x y â eq A y z â eq A x zâA.âa.â P:A âProp.P x âây.eq A x y â P yâA.âa.â P:A âProp.P x âây.eq A y x â P y
+ âA.âa.â P:A âSet.P x âây.eq A x y â P y
+ âA.âa.â P:A âSet.P x âây.eq A y x â P y
+ âA.âa.â P:A âType.P x âây.eq A x y â P y
+ âA.âa.â P:A âType.P x âây.eq A y x â P y
+ âA.âB.â f:A â B.âx,y:A.eq A x y â eq B (f x) (f y)
+ âA.âB.â f:A â B.âx,y:A.eq A x y â eq B (f y) (f x)true
@@ -242,8 +316,7 @@
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 and if it is handled by a
- development.
+ if it is not compiled yet.
@@ -270,36 +343,6 @@
-
- set
- set "baseuri" "s"
-
-
-
- Synopsis:
-
- set &qstring; &qstring;
-
-
-
- Action:
-
- Sets to s the baseuri of all the
- theorems and definitions stated in the current file.
- The baseuri should be a/b/c/foo
- if the file is named foo and it is in
- the subtree a/b/c of the current
- development.
- This requirement is not enforced, but it could be in the future.
-
- Currently, baseuri is the only
- property that can be set even if the parser accepts
- arbitrary property names.
-
-
-
-
- whelpwhelp locate "s"
@@ -336,7 +379,7 @@
qed
-
+ qed
@@ -358,5 +401,188 @@
-
+
+
+ inline
+ inline "s" params
+
+
+
+ Synopsis:
+
+
+ inline &qstring; &inlineparams;
+
+
+
+
+ Action:
+
+ Inlines a representation of the item s,
+which can be the URI of a HELM object. If an entire HELM directory (i.e. a base
+URI) or the path of a *.ma source file is provided, all the contained objects
+are represented in a row.
+If the inlined object has a proof, this proof is represented in several ways
+depending on the provided parameters.
+
+
+
+
+
+
+ inline-params
+