Matita Home

`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**.

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