next up previous contents index
Next: Formation Up: Details of the Previous: Computation System Modification

Inductive Type Proof Rules

The   proof rules will ensure that the following two assertions hold.

rec(x,y.A;b) type
& x:(B->Uk)->y:B->A type

rec(x,y.A;b) rec(x,y.A;b) type
& \y .rec(x,y.A;y)

That is, rec(x,y.A;b) is a type exactly when there is a type B and universe level k such that b is in B and for all x which, when instantiated with a value from B, yield a type at universe k, and y of type b, A (with x and y potentially free) is a type. Also, t is of type rec(x,y.A;b) exactly when rec(x,y.A;b) is a type and t is a member of the ``unwinding'' of the recursive type.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995