coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq Proof Assistant Question

From: Asya Bergal <abergal AT mit.edu>
To: coq-club AT inria.fr
Cc: "Dr. Damian Dechev" <dechev AT cs.ucf.edu>
Subject: Re: [Coq-Club] Coq Proof Assistant Question
Date: Tue, 9 Aug 2016 12:24:54 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=asyabergal AT gmail.com; spf=Pass smtp.mailfrom=asyabergal AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f182.google.com
Ironport-phdr: 9a23:CDEaRB3KixFktUpasmDT+DRfVm0co7zxezQtwd8ZsegRKvad9pjvdHbS+e9qxAeQG96KsrQc0qGO7eigATVGusfZ9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oMyKJV0Rz2LjKfMqdVPt/F2X7pFXyaJZaY8JgiPTpXVJf+kEjUhJHnm02yjG28Gr4ZR4+D5Rsf9yv+RJUKH9YrhqBecAVGduGykP6cbqrRjOSxeUrjtZCz1O00kAPw+Q5xbjG5z1ryHSt+xn2SDcM9elY6ozXGGL9LZiADXlkigOM3Zt+WvakMN5iIpeoQ7nqhBild2HKLqJPeZzK/uONegRQnBMC4MID3RM

In your example, "unfold program1" will show you the list.

On Tue, Aug 9, 2016 at 11:31 AM, Christina Peterson <clp8199 AT knights.ucf.edu> wrote:

Hello,

I am working with a record in the Coq Proof Assistant and would like to be able to access and display elements of the record in the proof environment so that I can apply formal logic to them. I have attached the file Example.v which is a simple reproducible example of the problem.

Sincerely,

Christina

[Coq-Club] Coq Proof Assistant Question, Christina Peterson, 08/09/2016
- Re: [Coq-Club] Coq Proof Assistant Question, Asya Bergal, 08/09/2016
- Re: [Coq-Club] Coq Proof Assistant Question, Tej Chajed, 08/09/2016