The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

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?