In order to define a function by induction on an inductive type
The syntax for an inductive definition looks as follows:
inductive_definition
<name>
(<parameter list>
): <indTp>
(<values of parameters of indTp>
) =
<tpl>
: <tp>
= <Tp>
![
\RS](/doc/img/RS.png)
<con>
: <args> ⟶ <tp>
= <def>
![
\RS](/doc/img/RS.png)
<out>
: <args2> ⟶ <tp2>
= <def2>
![
\RS](/doc/img/RS.png)
…
Here <indTp>
is a reference to an inductive type initialised to its parameter list. This reference list must provide a value for each parameter of the inductive type <indTp>
.
The types of the internal declarations given here can also be automatically inferred from the inductive type and don’t need to be given by the user. As with inductive types, the parameters in the <parameter list>
can be used anywhere in the body of the derived declaration, additionally they can also be used in the definition of the parameters used to initialize the inductive type.
Inductive definitions are elaborated to the following delarations:
<indTp>