The Coq mailing list

[roconnor AT theorem.ca]

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)

I should also mention that my motivation for wanting non-uniform 
parameters comes from the fact that the universe levels don't increase as 
much as they do with type families.  This prevents a Universe 
Inconsistentcy that would otherwise eventually appear during a development 
of the lambda calculus.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''