coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Non-uniform parameters in inductive definitions?

From: Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Non-uniform parameters in inductive definitions?
Date: Sun, 20 Nov 2011 20:36:22 -0400

>> 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.

[Coq-Club] Non-uniform parameters in inductive definitions?, Peter LeFanu Lumsdaine
- Re: [Coq-Club] Non-uniform parameters in inductive definitions?, Matthieu Sozeau
- <Possible follow-ups>
- Re: [Coq-Club] Non-uniform parameters in inductive definitions?, Bruno Barras
  - Re: [Coq-Club] Non-uniform parameters in inductive definitions?, roconnor
  - Message not available
    - Re: [Coq-Club] Non-uniform parameters in inductive definitions?, Bruno Barras
      - Re: [Coq-Club] Non-uniform parameters in inductive definitions?, Peter LeFanu Lumsdaine
        
        Re: [Coq-Club] Non-uniform parameters in inductive definitions?, Andreas Abel
        
        Re: [Coq-Club] Non-uniform parameters in inductive definitions?, Altenkirch Thorsten
- Re: [Coq-Club] Non-uniform parameters in inductive definitions?, Altenkirch Thorsten
  - Re: [Coq-Club] Non-uniform parameters in inductive definitions?, Andreas Abel