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

Datasyntax-ce-cc-nd-ty =

constr-def-ci-ni : expr

|constr-def-ci-ni : expr|constr-def-ci-niofexprandexpr ...

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