coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Paolo Herms <paolo.herms AT cea.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] inductive-coinductive ??
- Date: Mon, 27 Jun 2011 11:16:26 +0200
You mean something like this?
Section AccessibiltyFunctions.
Variable A : Type.
Variable f : A → A.
Variable start : A.
Inductive AccF : A → Prop :=
| AccF_start : AccF start
| AccF_cont a: AccF a → AccF (f a).
End AccessibiltyFunctions.
AccF f a defines the set of elements accessible by iterating f starting from
a.
--
Paolo Herms
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
Paris, France
- [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.