X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fhelp%2FC%2Fsec_commands.xml;h=1644c85bd88493728d926261f9b32211cb123a2c;hb=1eb77ed6774cb642e763182e900f143a0184e085;hp=0c8fdb4556f7adf8edffab9e42beae86ea746aaf;hpb=26d70cfe7b6cfd9518bdfe6709532b55e6ea2cc7;p=helm.git
diff --git a/matita/help/C/sec_commands.xml b/matita/help/C/sec_commands.xml
index 0c8fdb455..1644c85bd 100644
--- a/matita/help/C/sec_commands.xml
+++ b/matita/help/C/sec_commands.xml
@@ -9,13 +9,13 @@
alias num (instance n) = "def"
-
+ Synopsis:alias
- [id"&string;"="&string;"
- | symbol"&string;" [(instance &nat;)] ="&string;"
- | num [(instance &nat;)] ="&string;"
+ [id &qstring; = &qstring;
+ | symbol &qstring; [(instance &nat;)] = &qstring;
+ | num [(instance &nat;)] = &qstring;
]
@@ -57,11 +57,10 @@
check t
-
+ Synopsis:
- check &term;
-
+ check &term;
@@ -80,11 +79,10 @@
coercion u
-
+ Synopsis:
- coercion &uri;
-
+ coercion &uri;
@@ -112,20 +110,82 @@
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
+
+
+
+
+ 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
+
+
+ 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
+
+
+
+
+
+
+
+
@@ -136,7 +196,7 @@
hint
-
+ Synopsis:hint
@@ -159,41 +219,52 @@
include
-
+ include "s"
-
+ Synopsis:
- include
-
+ include &qstring;Action:
- &TODO;
+ Every coercion,
+ notation and
+ interpretation that was active
+ when the file s was compiled last time
+ is made active. The same happens for declarations of
+ default definitions and
+ theorems and disambiguation
+ 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 and if it is handled by a
+ development.
+
- include'
+ include' "s"
-
+ Synopsis:
- include'
-
+ include' &qstring;Action:
- &TODO;
+ Not documented (&TODO;), do not use it.
@@ -201,20 +272,29 @@
set
-
+ set "baseuri" "s"
-
+ Synopsis:
- set
-
+ set &qstring; &qstring;Action:
- &TODO;
+ 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.
@@ -222,20 +302,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.
+
@@ -246,7 +339,7 @@
-
+ Synopsis:qed