Matita HomeMatita Homedefinition f: T ≝ t
f is defined as t; T is its type. An error is raised if the type of t is not convertible to T.
T is inferred from t if omitted.
t can be omitted only if T is given. In this case Matita enters in interactive mode and f must be defined by means of tactics.
Notice that the command is equivalent to theorem f: T ≝ t.
discriminator i
Defines a new discrimination (injectivity+conflict) principle à la McBride for the inductive type i.
The principle will use John Major's equality if such equality is defined, otherwise it will use Leibniz equality; in the former case, it will be called i_jmdiscr, in the latter, i_discr. The command will fail if neither equality is available.
Discrimination principles are used by the destruct tactic and are usually automatically generated by Matita during the definition of the corresponding inductive type. This command is thus especially useful when the correct equality was not loaded at the time of that definition.
inverter n for i (path) : s
Defines a new induction/inversion principle for the inductive type i, called n.
(path) must be in the form (# # # ... #), where each # can be either ? or %, and the number of symbols is equal to the number of right parameters (indices) of i. Parentheses are mandatory. If the j-th symbol is %, Matita will generate a principle providing equations for reasoning on the j-th index of i. If the symbol is a ?, no corresponding equation will be provided.
s, which must be a sort, is the target sort of the induction/inversion principle and defaults to Prop.
inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'
Declares a family of two mutually inductive types i and i' whose types are S and S', which must be convertible to sorts.
The constructors ki of type Ti and ki' of type Ti' are also simultaneously declared. The declared types i and i' may occur in the types of the constructors, but only in strongly positive positions according to the rules of the calculus.
The whole family is parameterized over the arguments x,y,z.
If the keyword coinductive is used, the declared types are considered mutually coinductive.
Elimination principles for the record are automatically generated by Matita, if allowed by the typing rules of the calculus according to the sort S. If generated, they are named i_ind, i_rec and i_rect according to the sort of their induction predicate.
record id x y z: S ≝ { f1: T1; …; fn:Tn }
Declares a new record family id parameterized over x,y,z.
S is the type of the record and it must be convertible to a sort.
Each field fi is declared by giving its type Ti. A record without any field is admitted.
Elimination principles for the record are automatically generated by Matita, if allowed by the typing rules of the calculus according to the sort S. If generated, they are named i_ind, i_rec and i_rect according to the sort of their induction predicate.
For each field fi a record projection fi is also automatically generated if projection is allowed by the typing rules of the calculus according to the sort S, the type T1 and the definability of depending record projections.
If the type of a field is declared with :>, the corresponding record projection becomes an implicit coercion. This is just syntactic sugar and it has the same effect of declaring the record projection as a coercion later on.