The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

All the papers I could find about inductive constructions seem to present
the elimination scheme as an integrated induction operator "Elim".

In Coq, on the other hand, I can use "Fixpoint" and "match" as two separate
constructs, to write my inductions mush as I would do in ML.

Could someone point me to a paper presenting formally the constraints placed
on the use of "match" and "Fixpoint" to guarantee termination (in Coq or in
some simplified variant)?  Ideally, this paper would come with a proof of
strong normalization (maybe via reducibility to the usual Elim form).


        Stefan