X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=19685bf9034e167fd0f4744501dd8ad390a3b7a6;hb=04133d1b68fbde1fada8fe793eea265e8849af8d;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..19685bf90 100644 --- a/helm/software/matita/help/C/sec_commands.xml +++ b/helm/software/matita/help/C/sec_commands.xml @@ -2,6 +2,404 @@ 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 + + + + + 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. + + + + +