coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Why can Records not be recursive?

From: Gregory Malecha <gmalecha AT cs.harvard.edu>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Why can Records not be recursive?
Date: Thu, 2 Oct 2014 10:46:08 -0400

Hi --

Is the a theoretical reason why records can not be recursive? My understanding has always been that [Record] is just syntactic sugar for [Inductive] which generates some extra projection functions. I know that this will change in Coq 8.5 and records will become a new primitive, so will there become a reason why they can't be recursive?

Thanks.

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/

[Coq-Club] Why can Records not be recursive?, Gregory Malecha, 10/02/2014
- Re: [Coq-Club] Why can Records not be recursive?, Cedric Auger, 10/02/2014
  - Re: [Coq-Club] Why can Records not be recursive?, Arnaud Spiwack, 10/02/2014
    - Re: [Coq-Club] Why can Records not be recursive?, Gregory Malecha, 10/02/2014
      - Re: [Coq-Club] Why can Records not be recursive?, Jason Gross, 10/02/2014