The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On Thu, 12 May 2011 14:39:29 +0200, 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?

I don't know whether allowing recursive records would be useful.

However,

Existing Class Acc.

seems to work, turning Acc into a class.

  Tom