To define a constant, one may use the `define`

command:

```
define /double/
/ fn x . x + x /
/ nat -> nat /;
```

The first argument is the constant being defined, the second gives the
definition, and the third gives its type. Istari will then begin a
proof wherein you can prove that `double`

has the type `nat -> nat`

.

You can also define a constant that takes arguments. For example, the same definition could be written:

```
define /double x/
/ x + x /
/ nat -> nat /;
```

Note that the type argument is unchanged from before; it is the type
of `double`

, not the type of `double x`

.

A definition can also take **implicit arguments**, such as:

```
define /double_list {a} l/
/ ` append a l l /
/ intersect (i : level) . forall (a : U i) . list a -> list a /;
```

Here `a`

is an implicit argument. Whenever `double_list`

is used, the
parser will insert evars for each implicit argument. One can suppress
the insertion of implicit arguments using the tick symbol (```

).

In the example, tick is used to suppress the implicit argument of
`append`

, allowing us to specify it explicitly.

One can also define a constant without a type, using the command
`defineRaw`

. Then, if desired, one can attach a type to the constant
after the fact using by proving a typing lemma and attaching it using
`recordTyping`

:

```
lemma "double_type"
/ double : nat -> nat /;
... do the proof ...
qed ();
recordTyping "double_type";
```

There is a hazard to using raw definitions: Constant definitions are not permitted to contain evars. With an ordinary definition, any evars (such as those arising from calling functions with implicit arguments) would typically be instantiated in the course of establishing the constant’s type. But in a raw definition one must be sure to avoid creating evars.

One can define a recursive function using a regular definition and
`fix`

, but Istari offers a more convenient syntax:

```
definerec /length {a} l/
/ list_case l 0 (fn h t . succ (length a t)) /
/ intersect (i : level) . forall (a : U i) . list a -> nat /;
```

Note that `length`

’s implicit argument `a`

is still explicit during
the definition.

A recursive definition not only creates the constant, it also creates
an unrolling rewrite. If one uses the `unfold`

rewrite on (say)
`` length a l`

, one gets the underlying fixpoint term:

```
fix (fn length1 a l . list_case l 0 (fn h t . succ (length1 a t))) a l
```

but using `unroll`

results in a much cleaner term:

```
list_case l 0 (fn h t . succ (` length a t))
```

One can also make recursive definitions without a type using the
command `definerecRaw`

, subject to the same free evar hazard discussed
above.

One can define mutually recursive definitions using a recursive definition of a tuple, but again Istari offers a more convenient syntax:

```
definemutrecRaw /x/
/
snork1 y =
if Nat.eqb y 0 then
x
else
snork2 y
and
snork2 y = snork1 (y - 1) * 2
/;
```

Here, `x`

is a pervasive argument that is available to all of the
mutually defined functions. Thus `snork1`

and `snork2`

have the type
`nat -> nat -> nat`

(although this has to be proven, of course).

The definition also creates an appropriate unrolling rewrite. If one
uses `unfold /snork2/`

on the goal:

```
snork2 4 2 = 16 : nat
```

one obtains:

```
snork1 4 (2 - 1) * 2 = 16 : nat
```

For mutually recursive definitions, there is only the raw version. To
give mutually recursive definitions a type, one must prove a typing
lemma and then install it using `recordTyping`

. Again, this is
subject to the free evar hazard.

One defines datatypes with the `typedef`

command. For example:

```
typedef
/
datatype
intersect (i : level) .
forall (a : U i) .
U i
of
tree : nat -> type =
| Empty : tree 0
| Node : forall (n : nat) . a -> forest n -> tree (succ n)
and
forest : nat -> type =
| Nil : forest 0
| Cons : forall (m n : nat) . tree m -> forest n -> forest (m + n)
/;
```

A datatype definition begins with “invisible” pervasive arguments
preceded by the `intersect`

keyword. They are `intersect`

-bound in
the types of the datatypes and constructors. (This is typically used
for level variables.) Next are the visible pervasive arguments,
preceded by the `forall`

keyword. They are arguments to all the
datatypes and constructors. Next is the universe to which the
datatypes belong. In the example, the datatypes belong to the same
universe (`U i`

) to which the type argument `a`

belongs.

Next are the datatype and their constructors. Each datatype can take
additional “index” arguments. In the example, both datatypes take
`nat`

. Thus, they each have the type:

```
intersect (i : level) . forall (a : U i) . nat -> U i
```

The constructors can take “external” and “internal” arguments. The
external argument’s types are unrestricted, except they cannot mention
the datatypes being defined. The internal argument’s types must be
the datatypes being defined. External arguments can be dependent (as
in `m`

and `n`

in the example), but internal arguments must be
non-dependent.

In the example, the constructors have type:

```
Empty : intersect (i : level) . forall (a : U i) . tree a 0
Node : intersect (i : level) . forall (a : U i) (n : nat) . a -> forest a n -> tree a (succ n)
Nil : intersect (i : level) . forall (a : U i) . forest a 0
Cons : intersect (i : level) . forall (a : U i) (m n : nat) . tree a m -> forest a n -> forest a (m + n)
```

Defining a datatype incurs several typing obligations. With
`typedef`

, those obligations are discharged automatically by the
typechecker if possible. With `typedefRaw`

they are all handed over
to the user.

For more discussion of how datatypes are used, see the datatypes page.

To define new reductions to be used automatically by the normalization
engine, one may use the `reductions`

command:

```
reductions
/
length _ (nil _) --> 0 ;
length a (cons _ h t) --> succ (length a t) ;
unrolling length
/;
```

To establish that the specified reductions are correct, the prover
places the left- and right-hand-side into normal form and compares
them. The `unrolling`

clause indicates that, while normalizing, the
prover should unroll `length`

. One can also employ an `unfolding`

clause to indicate that the prover should unfold certain identifiers.
An `unrolling`

clause will be applied only once (to avoid looping),
and only on the left-hand-side. In contrast, an `unfolding`

clause
will be applied at every opportunity.

The left-hand-sides of reductions take a special syntax: they must
consist of a constant followed by a list of arguments. Amidst the
arguments is exactly one *principal* argument (`nil _`

and ```
cons _ h
t
```

in the example). The principal argument must be parenthesized,
even if it takes no arguments.

The right-hand-side uses the ordinary term syntax, except that implicit arguments are not inserted. (An evar on the right-hand-side would never be correct.)

Note that the process of verifying reductions is purely syntactic, so it can be sensitive to subtle changes. For example, this variation on the second reduction, though deceptively similar, is incorrect:

```
length _ (cons a h t) --> succ (length a t) ; (* incorrect *)
```

The right-hand-side of a reduction should not contain an instance of
the left-hand-side (even beneath a lambda). Such a reduction (if
valid) *will* be accepted, but it will result in normalization
looping. Since unification tries to avoid normalizing, the
non-terminating behavior might not arise for some time, making its
cause not obvious when it finally does.

To define an inductive function, one can make an ordinary definition using a datatype iterator. However, Istari provides a command to streamline the process:

```
defineInd /a/
/
treesize : tree [a] __ -> nat of
| Empty . 0
| Node _ x f . succ (forestsize f)
| One _ t . treesize t
and
forestsize : forest __ -> nat of
| Nil . 0
| Cons _ _ t f . treesize t + forestsize f
/
/
intersect i . forall (a : U i) n . tree a n -> nat
and
intersect i . forall (a : U i) n . forest a n -> nat
/;
```

This defines multiple inductive functions simultaneously, installs the
appropriate reductions, and attempts to prove the
typing lemmas. The syntax of the inductive functions is discussed
here. (Note that the keyword
`fnind`

is dropped.)

The first argument to `defInd`

(in the example, `a`

) gives a list of
arguments that each inductive function should take. Those arguments
are available to the pervasive arguments (`[a]`

), and to the arms of
the inductive functions (not used in this example). The second
argument gives the inductive functions, and the third argument gives
their types, as a list separated by `and`

.

In addition to installing the appropriate reductions, it writes them to the registry. For example:

```
treesize _ _ (Empty _) --> 0
```

is written using the name `treesize_Empty`

.