The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

I don't understand this description of fixpoint reduction from p. 134
of the Reference Manual (.pdf, version 8.5pl1).

====================================
Let F be the set of declarations: f1/k1:A1 := t1 ... fn/kn:An := tn.
The reduction for fixpoints is:

(Fix fi{F} a1 . . . aki)  >_i
       ti {(fk /Fix fk {F})k=1...n} a1 . . . aki

when aki starts with a constructor. This last restriction is needed
in order to keep strong normalization and corresponds to the reduction
for primitive recursive operators.
====================================

Is a_{k_i} in the reduction rule a typo?  Can someone explain the
phrase "and corresponds to the reduction
for primitive recursive operators".

Thanks,
Randy
--