X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=5e55de9994648e7768358c6751f7eb2b96dbb589;hb=6067115471521e8b9ea805531cb94a0a80774314;hp=7141d0ddffd1ff22dab3ded1fa43c6521f564fcf;hpb=33f739f6354adaf949cb6c1e8e57f742c0d88bf0;p=helm.git
diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml
index 7141d0ddf..5e55de999 100644
--- a/helm/software/matita/help/C/sec_commands.xml
+++ b/helm/software/matita/help/C/sec_commands.xml
@@ -9,7 +9,7 @@
alias num (instance n) = "def"
-
+ Synopsis:alias
@@ -57,7 +57,7 @@
check t
-
+ Synopsis:check &term;
@@ -79,7 +79,7 @@
coercion u
-
+ Synopsis:coercion &uri;
@@ -110,20 +110,94 @@
default
-
+ default "s" u1 ⦠un
-
+ Synopsis:default
+ &qstring; &uri; [&uri;]â¦
Action:
- &TODO;
+ It registers a cluster of related definitions and
+ theorems to be used by tactics and the rendering engine.
+ Some functionalities of Matita are not available when some
+ clusters have not been registered. Overloading a cluster
+ registration is possible: the last registration will be the
+ default one, but the previous ones are still in effect.
+
+ s is an identifier of the cluster and
+ u1 ⦠un
+ are the URIs of the definitions and theorems of the cluster.
+ The number n of required URIs depends on the
+ cluster. The following clusters are supported.
+
+
+ clusters
+
+
+
+ name
+ expected object for 1st URI
+ expected object for 2nd URI
+ expected object for 3rd URI
+ expected object for 4th URI
+ expected 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
+
+
+
+
+ equality
+ an inductive type (say, of type eq) of type âA:Type.A âProp with one family parameter and one constructor of type âx:A.eq A x
+ a theorem of type âA.âx,y:A.eq A x y â eq A y x
+ 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
+ an inductive type of type Prop with only one constructor that has no arguments
+
+
+
+
+
+
+ false
+ an inductive type of type Prop without constructors
+
+
+
+
+
+
+ absurd
+ a theorem of type âA:Prop.âB:Prop.A â Not A â B
+
+
+
+
+
+
+
+
@@ -134,7 +208,7 @@
hint
-
+ Synopsis:hint
@@ -160,7 +234,7 @@
include "s"
-
+ Synopsis:include &qstring;
@@ -193,7 +267,7 @@
-
+ Synopsis:include' &qstring;
@@ -213,7 +287,7 @@
set "baseuri" "s"
-
+ Synopsis:set &qstring; &qstring;
@@ -240,20 +314,33 @@
whelp
-
+ whelp locate "s"
+ whelp hint t
+ whelp elim t
+ whelp match t
+ whelp instance t
-
+ Synopsis:whelp
+ [locate &qstring;
+ | hint &term;
+ | elim &term;
+ | match &term;
+ | instance &term;
+ ]
Action:
- &TODO;
+ Performs the corresponding query,
+ showing the result in the CIC browser. The command is removed
+ from the script.
+
@@ -264,7 +351,7 @@
-
+ Synopsis:qed