X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=7e22f33043d39ec5e0fcb62e7ce0c20ca1e41593;hb=d8bc6fd4ab18f2995624c75e2889318237e9c17f;hp=b1bada0fddb9a06c348d8739c3ff639750155fc7;hpb=c52baa34c7363fa58f81aea95bb0d72e10afdaf1;p=helm.git
diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml
index b1bada0fd..7e22f3304 100644
--- a/helm/software/matita/help/C/sec_commands.xml
+++ b/helm/software/matita/help/C/sec_commands.xml
@@ -2,6 +2,587 @@
Other commands
- &TODO;
-
+
+ alias
+ alias id "s" = "def"
+ alias symbol "s" (instance n) = "def"
+ alias num (instance n) = "def"
+
+
+
+ Synopsis:
+
+ alias
+ [id &qstring; = &qstring;
+ | symbol &qstring; [(instance &nat;)] = &qstring;
+ | num [(instance &nat;)] = &qstring;
+ ]
+
+
+
+
+ Action:
+
+ Used to give an hint to the disambiguating parser.
+ When the parser is faced to the identifier (or symbol)
+ s or to any number, it will prefer
+ interpretations that "map s (or the
+ number) to def". For identifiers,
+ "def" is the URI of the interpretation.
+ E.g.: cic:/matita/nat/nat.ind#xpointer(1/1/1)
+ for the first constructor of the first inductive type defined
+ in the block of inductive type(s)
+ cic:/matita/nat/nat.ind.
+ For symbols and numbers, "def" is the label used to
+ mark the wanted
+ interpretation.
+
+ When a symbol or a number occurs several times in the
+ term to be parsed, it is possible to give an hint only for the
+ instance n. When the instance is omitted,
+ the hint is valid for every occurrence.
+
+
+ Hints are automatically inserted in the script by Matita every
+ time the user is interactively asked a question to disambiguate
+ a term. This way the user won't be posed the same question twice
+ when the script will be executed again.
+
+
+
+
+
+
+ check
+ check t
+
+
+
+ Synopsis:
+
+ check &term;
+
+
+
+ Action:
+
+ Opens a CIC browser window that shows t
+ together with its type. The command is immediately removed from
+ the script.
+
+
+
+
+
+
+ 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 with ariety saturation nocomposites
+
+
+
+ Synopsis:
+
+
+ coercion
+ (&uri; | &term; with)
+ [ &nat; [&nat;]]
+ [ nocomposites ]
+
+
+
+
+ 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
+ automatically replaces x with
+ (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.
+ When a coercion u is declared
+ from source s to target t
+ and there is already a coercion u' of
+ target s or source t,
+ a composite implicit coercion is automatically computed
+ by Matita unless nocomposites
+ is specified.
+
+
+
+
+
+
+ default
+ default "s" u1 ⦠un
+
+
+
+ Synopsis:
+
+ default
+ &qstring; &uri; [&uri;]â¦
+
+
+
+
+ Action:
+
+ 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
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ hint
+ hint
+
+
+
+ Synopsis:
+
+ hint
+
+
+
+
+ Action:
+
+ Displays a list of theorems that can be successfully
+ applied to the current selected sequent. The command is
+ removed from the script, but the window that displays the
+ theorems allow to add to the script the application of the
+ selected theorem.
+
+
+
+
+
+
+
+ include
+ include "s"
+
+
+
+ Synopsis:
+
+ include &qstring;
+
+
+
+ Action:
+
+ 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.
+
+
+
+
+
+
+
+ include' "s"
+
+
+
+
+ Synopsis:
+
+ include' &qstring;
+
+
+
+ Action:
+
+ Not documented (&TODO;), do not use it.
+
+
+
+
+
+
+ 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:
+
+ Performs the corresponding query,
+ showing the result in the CIC browser. The command is removed
+ from the script.
+
+
+
+
+
+
+
+ qed
+ qed
+
+
+
+ Synopsis:
+
+ qed
+
+
+
+
+ Action:
+
+ Saves and indexes the current interactive theorem or
+ definition.
+ In order to do this, the set of sequents still to be proved
+ must be empty.
+
+
+
+
+
+
+
+ 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
+