coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] dependent types and inversion

From: Conor McBride <c.t.mcbride AT durham.ac.uk>
To: coq-club AT pauillac.inria.fr
Cc: Dimitri Hendriks <hendriks AT cs.kun.nl>
Subject: [Coq-Club] dependent types and inversion
Date: Wed, 24 Dec 2003 13:35:32 +0000
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi

Sorry to take so long...

Dimitri writes

> Is there a way to work around this (without using axioms
> as in Eqdep.v or JMeq.v)?

I'm afraid not. It's exactly this kind of problem that JMeq was
invented to solve.

I suggest that using suitable definitions and restating the lemmas
will be less work in the long run.

Merry Christmas

Conor

[Coq-Club] dependent types and inversion, Dimitri Hendriks
- <Possible follow-ups>
- [Coq-Club] dependent types and inversion, Conor McBride