next up previous contents index
Next: Inductive Type Proof Up: Details of the Previous: Details of the

Computation System Modification

Add terms

rec_ind( r; v,u.g)
where u,v,x and z range over variables, a,g,r and T range over terms, and T is restricted as follows:
No instance of z bound by rec may occur in the domain type of a function space, in the argument of a function application or in the principal argument(s) of the remaining elimination forms.gif
Thus (A#z)->B or f(inr z) or spread(z; a,b.a->int)\ cannot be subexpressions of T. When closed, rec terms are canonical and rec_ind terms are noncanonical. These noncanonical terms are redices  with principal argument r and contracta 
\u.rec_ind( u; v,u.g),
when r is canonical. The rules for binding  variables are:

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