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: C T McBride <c.t.mcbride AT durham.ac.uk>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Pattern matching while defining a type
Date: Thu, 31 Oct 2002 17:18:28 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, Oct 23, 2002 at 04:52:28PM +0100, C T McBride wrote:

> Subject to `size of type' restrictions, it is possible to turn
> inductive-recursive definitions into inductive families.

> I don't pretend that this is pretty, but if you haven't got
> induction-recursion, then it may be worth considering this fake.

Thank you for this information. For my use, I have decided to simply
drop the "recursive" part of my inductive-recursive definition, giving
a type T, define my constraint "c" (the recursive part of the
inductive-recursive definition) and use explicit additional hypotheses
"(c t)" for my objects of type T in my theorems.

--
Lionel

Attachment: pgpmNocqYAWpa.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