coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Pattern matching while defining a type

From: Lionel Elie Mamane <lionel AT mamane.lu>
To: Frederic Blanqui <blanqui AT lix.polytechnique.fr>, Venanzio Capretta <Venanzio.Capretta AT sophia.inria.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Pattern matching while defining a type
Date: Tue, 22 Oct 2002 19:25:10 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Tue, Oct 22, 2002 at 05:11:06PM +0200, Frederic Blanqui wrote:

> This is what is called an inductive-recursive type. See:

On Tue, Oct 22, 2002 at 04:58:33PM +0200, Venanzio Capretta wrote:

> This kind of definitions is not permitted in Coq, but it is allowed in
> systems that admits simultaneous induction-recursion like ALF.

Thank you for your answers. I will now:

- Work around the problem by defining my type without the constraint,
and adding "check" hypotheses to my theorems.

- Read the paper (and possibly some neighbours in the "cites / is
cited by" graph) you cited because it looks interesting.

--
Lionel

Attachment: pgp2a6wrfPEma.pgp
Description: PGP signature

[Coq-Club] Pattern matching while defining a type, Lionel Elie Mamane
- Message not available
  - Re: [Coq-Club] Pattern matching while defining a type, Lionel Elie Mamane
    - Re: [Coq-Club] Pattern matching while defining a type, Frederic Blanqui
      - Re: [Coq-Club] Pattern matching while defining a type, Lionel Elie Mamane
        
        Re: [Coq-Club] Pattern matching while defining a type, C T McBride
        
        Re: [Coq-Club] Pattern matching while defining a type, Lionel Elie Mamane
    - Re: [Coq-Club] Pattern matching while defining a type, Eduardo Gimenez
      - Re: [Coq-Club] Pattern matching while defining a type, Lionel Elie Mamane
- Re: [Coq-Club] Pattern matching while defining a type, Venanzio Capretta