coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A non well-founded set

From: Pat Castelnau <dfzone-coq AT yahoo.fr>
To: Matthieu Sozeau <sozeau AT lri.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] A non well-founded set
Date: Sat, 5 Apr 2008 11:18:08 +0000 (GMT)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.fr; h=X-YMail-OSG:Received:X-Mailer:Date:From:Reply-To:Subject:To:Cc:In-Reply-To:MIME-Version:Content-Type:Content-Transfer-Encoding:Message-ID; b=Vx9ucslHmZRM2Bo2uhRhKur9HY3oU/KVS7Li7V9zu0a0A4BvMfYt4oN2GpR8MWxntID8hhj98nZg+gbewaBCZZhAhsMwhRrSDv4j7C/D7pggBgXm/y1Uk+UBFxaTbP7AbZ5JXhTQo6xdRk6Oych9ttg7VgXyKL/hjr8hhadN+6o=;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Thanks for your help!

Matthieu Sozeau wrote:
> Using a function instead ?

And then, how do you take the greatest fixpoint of F?

> I'm not sure which type you want f and F(X) to have ?

F:Type->Type and f:nat->X->Prop.

Although it is not accepted by Coq, the coinductive definition I gave in my
first email should tell you what I want.

_____________________________________________________________________________
Envoyez avec Yahoo! Mail. Une boite mail plus intelligente
http://mail.yahoo.fr

[Coq-Club] A non well-founded set, Pat Castelnau
- Re: [Coq-Club] A non well-founded set, Bruno Barras
- <Possible follow-ups>
- Re: [Coq-Club] A non well-founded set, Pat Castelnau