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
inl 2,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 as
inr <inl 3,inl 5> and
inr <inr <inl 7,inl 11>,inl 13>.
rec(z,x. x | z(x)#z(x); int),and the predicate function dom,
asserting f has a root is denoted
\x. rec(dom,x. int_eq(f(x); 0; true; dom(x+1)); x).The elim form,
rec_ind, is analogous to the
tis of type
rec(z. int | z#z)then the following term computes the sum of the values at
rec_ind(t; sum,x. decide(x; leaf. leaf; pair. spread(pair; left_son,right_son. sum(left_son)+sum(right_son))))The simpler rec(z.T) form is not formally part of the extension since it can be mimicked by rec(z,x. Tz(0)z;0), for example, so consider any rec(z.T) term in what follows to be just an abbreviation. Inductive types can also be defined in a mutually recursive fashion, but we will not pursue that possibility here.