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