Definitions and declarations

axiom id: term

axiom H: P

H is declared as an axiom that states P

definition id[: term] [ term]

definition 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.

letrec TODO

TODO

[inductive|coinductive] id [args2]… : term [|] [id:term] [| id:term]… [with id : term [|] [id:term] [| id:term]…]…

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 [args2]… : term {[id [:|:>] term] [;id [:|:>] term]…}

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.