See Recursive Types for supplementary material.

As an introduction to the ` rec` types, consider
the inductive type of integer trees, defined informally as

In the language of ` rec` types this type may be defined as

rec(z. int | z#z).Its elements include

An inductive type may also be parameterized; generalizing the above definition of binary integer trees to general binary trees over a specified type, the example rephrased asinl 2,

inr <inl 3,inl 5>and

inr <inr <inl 7,inl 11>,inl 13>.

is denoted

rec(z,x. x | z(x)#z(x); int),and the predicate function

asserting

\x. rec(dom,x. int_eq(f(x); 0; true; dom(x+1)); x).The elim form,

`rec_ind`

, is analogous to the `list_ind`

and integer
`ind`

forms. If `t`

is of type `rec(z. int | z#z)`

then
the following term computes the sum of the values at `t`

's leaves.
rec_ind(t; sum,x. decide(x; leaf. leaf; pair. spread(pair; left_son,right_son. sum(left_son)+sum(right_son))))The simpler

Thu Sep 14 08:45:18 EDT 1995