X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=7e22f33043d39ec5e0fcb62e7ce0c20ca1e41593;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;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..7e22f3304 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; @@ -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 nocomposites - + Synopsis: - 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. @@ -110,20 +172,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 +270,7 @@ hint - + Synopsis: hint @@ -160,7 +296,7 @@ include "s" - + Synopsis: include &qstring; @@ -180,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. @@ -193,7 +328,7 @@ - + Synopsis: include' &qstring; @@ -208,80 +343,246 @@
- - set - set "baseuri" "s" + + whelp + whelp locate "s" + whelp hint t + whelp elim t + whelp match t + whelp instance t - + Synopsis: - set &qstring; &qstring; + whelp + [locate &qstring; + | hint &term; + | elim &term; + | match &term; + | instance &term; + ] + 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. + Performs the corresponding query, + showing the result in the CIC browser. The command is removed + from the script. - Currently, baseuri is the only - property that can be set even if the parser accepts - arbitrary property names. - - whelp - + + qed + qed - + Synopsis: - whelp + qed Action: - &TODO; + 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. - - qed - + + + inline + inline "s" params - + Synopsis: - qed + + inline &qstring; &inlineparams; 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. + 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 + + inline-params + + + + &inlineparams; + ::= + [&inlineparam; [&inlineparam;] … ] + + + +
+ + inline-param + + + + + &inlineparam; + ::= + axiom + Try to give an axiom flavour + (bodies are omitted even if present) + + + + + + | + definition + Try give a definition flavour + + + + + + | + theorem + Try give a theorem flavour + + + + + + | + lemma + Try give a lemma flavour + + + + + + | + remark + Try give a remark flavour + + + + + + | + fact + Try give a fact flavour + + + + + + | + variant + Try give a variant flavour + (implies plain) + + + + + + | + declarative + Represent proofs using + declarative tactics + (this is the dafault and can be omitted) + + + + + + | + procedural + Represent proofs using + procedural tactics + + + + + + | + plain + Represent proofs using plain + proof terms + + + + + + | + nodefaults + + Do not use the tactics depending on the + default command + (rewrite + in the procedural mode) + + + + + + | + level=&nat; + + Set the level of the procedural proof representation + (the default is the highest level) + + + Tactics used at level 1: + exact + + + Additional tactics used at level 2: + letin, + cut, + change, + intros, + apply, + elim, + cases, + rewrite + + + + + + + + | + depth=&nat; + &TODO; + + + + +
+
-