next up previous contents index
Next: Appendix A: Summary Up: Partial Function Type Previous: Elim

Computation

  .
  H,r:ind(z,x¯.T;a) >> Gagggggggby ind r over A 
 ¯[EXT foobar]¯[EXT foobar] H >> [a] = t in B 				 by reduce

>> = t in B



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