Skip to Content.
Sympa Menu

coq-club - [Coq-Club] inductive-coinductive ??

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] inductive-coinductive ??


chronological Thread 
  • 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.


 



Archive powered by MhonArc 2.6.16.

Top of Page