Next: Generation of LaTeX documents. Up: Inductive predicates and data-types. Previous: Inductive predicates.   Contents

# Inductive data-types.

The definition of inductive data-types is similar. Let us start with an example:

``` Data List A =
nil : List A nil
| cons x l : A x -> List A l -> List A (cons x l)
.
```

This example will generate a sort `list` with one parameter. It will create two constants `nil : list['a]` and `cons : 'a -> list['a] -> list['a]`.

It will also claim the axiom that these constants are distinct and injective.

Then it will proceed in the same manner as the following inductive definition to define the predicate `List` and the corresponding lemmas:

``` Inductive List A l =
nil : List A nil
| cons : /\x,l (A x -> List A l -> List A (cons x l))
.
```

There is also a syntax more similar to ML:

```type List A =
nil  List A nil
| cons of A and List A
.
```

The general syntax is (`Data` can be replaced by `type`):

 constr-def alpha-ident {ass-ident} `[` alpha-ident `]` syntax `Data` syntax `-ce` `-cc` `-nd` `-ty` = constr-def `-ci` `-ni` : expr `|` constr-def `-ci` `-ni` : expr `|` constr-def `-ci` `-ni` `of` expr `and` expr ...

We can remark three new options: `-nd` to tell PhoX not to generate the axioms claiming that all the constructors are distinct, `-ty` to tell PhoX to generate typed axioms (for instance `/\x:N (N0 != S x)` instead of `/\x (N0 != S x)`) and `-ni` to tell PhoX not to generate the axiom claiming that a specific constructor is injective.

One can also remark that we can give a special syntax to the constructor, but one still need to give an alphanumeric identifier (between square bracket) to generate the name of the theorems.

Here is an example with a special syntax:

```Data List A =
nil : List A nil
| [cons] rInfix[3.0] x "::" l : A x -> List A l -> List A (x::l)
.
```

Next: Generation of LaTeX documents. Up: Inductive predicates and data-types. Previous: Inductive predicates.   Contents
Christophe Raffalli 2005-03-02