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

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