The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

If you want some literature on this, I can advertise the paper by Ralph 
and myself:

Fixed Points of Type Constructors and Primitive Recursion
Andreas Abel and Ralph Matthes
Computer Science Logic, 18th International Workshop, CSL 2004, 13th 
Annual Conference of the EACSL
Karpacz, Poland, September 2004. LNCS 3210, © Springer.

http://www2.tcs.ifi.lmu.de/~abel/publications.html#csl04

It is about Fomega, no dependencies, but the principles stay the same 
for CC.

Cheers,
Andreas

On 21.11.11 2:36 AM, Peter LeFanu Lumsdaine wrote:
> > > On Wed, 16 Nov 2011, Bruno Barras wrote:
> > >
> > > > Putting what Matthieu already said with my own words:
> > > > non-uniform parameters behave
> > > > (1) like normal indices w.r.t. recursive schemes
> > > > (2) like parameters w.r.t. dependent pattern-matching (check out
> > > > list'_case)
>
> Many thanks to those who replied both on- and off-list; this makes a
> lot of sense now.
>
> Best,
> –Peter.

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/