Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] inductive-coinductive ??


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




Archive powered by MhonArc 2.6.16.

Top of Page