coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Recursive Class

From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
To: coqclub AT inria.fr
Cc: AUGER Cedric <Cedric.Auger AT lri.fr>
Subject: Re: [Coq-Club] Recursive Class
Date: Sat, 21 May 2011 10:55:01 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=D/E5oPABfOAXP3CSxJ/grPBxrdUlBXR3zd7/zN98z2rKk/XgSvAkN+WuTzT5uJkOO9 WEsecjWN5o/19lEewZzH52vq9nlVxsP8ZQ9TubNC+Q+oEeab97yU3eKyyjWCj4ehgZI+ lmFcUhF3LjMGXzn76Flwl+gY3cje+MaCThmTI=

Inductive Acc (X: Type) (P: X -> X -> Prop) (x: X) := Acc_intro {
wf: forall y, P x y -> Acc X P x
}.
(* Acc is defined
Acc_rect is defined
Acc_ind is defined
Acc_rec is defined
Acc_case is defined
wf is defined *)

On 12 May 2011 14:39, AUGER Cedric <Cedric.Auger AT lri.fr> wrote:

Hi all,
would it be possible to allow recursion in Records, Structure, Class,
so that the accessibility predicate may become a Class?

Class Acc (X: Type) (P: X → X → Prop) (x: X) := Acc_intro {
wf: forall y, P x y → Acc X P x
}.

Or is it considered useless in practice to have such a feature?

[Coq-Club] Recursive Class, AUGER Cedric
- Re: [Coq-Club] Recursive Class, Tom Prince
- Re: [Coq-Club] Recursive Class, Arnaud Spiwack