coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vladimir Voevodsky <vladimir AT ias.edu>
- To: Coq-Club Club <coq-club AT inria.fr>
- Subject: [Coq-Club] inductive-coinductive ??
- Date: Sun, 26 Jun 2011 20:30:24 -0400
Is there a way to define in Coq the type which can be informally described as
follows:
1. Given parameters A : Type , a : A .
2. I want to define the type of (infinite) sequences f_0 ,..., f_n, .... where
2a. f_0 : A -> A .
2b. f_{S n} : {| x : A ; f_n x = a |} -> A .
Is there a way to define the type of such sequences ?
Thanks!
Vladimir.
- [Coq-Club] inductive-coinductive ??, Vladimir Voevodsky
- Re: [Coq-Club] inductive-coinductive ??,
Andreas Abel
- Re: [Coq-Club] inductive-coinductive ??, Vladimir Voevodsky
- Re: [Coq-Club] inductive-coinductive ??,
AUGER Cedric
- Re: [Coq-Club] inductive-coinductive ??, AUGER Cedric
- <Possible follow-ups>
- Re: [Coq-Club] inductive-coinductive ??, Paolo Herms
- Re: [Coq-Club] inductive-coinductive ??,
Andreas Abel
Archive powered by MhonArc 2.6.16.