coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] obligations

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] obligations
Date: Wed, 11 May 2016 09:56:58 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f48.google.com
Ironport-phdr: 9a23:pRzYShboAqXHLQ36BFgtHyz/LSx+4OfEezUN459isYplN5qZpc+5bnLW6fgltlLVR4KTs6sC0LqH9fm+EjVYud6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDjvcSNKFwQ3HKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzAomxZJBkD35RX7QJ655jXov+58xiCyNsjrC704RGLxvO9QVBb0hXJfZHYC+2bNh5kogQ==

On Tue, May 10, 2016 at 9:32 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

as said on the bug report, you can use Program Definition instead:

Program Definition kp_assoc
(xr xc yr yc zr zc: nat)
(x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc) :
kp x (kp y z) = kp (kp x y) z := _.

Thanks! It would be very helpful if Program will work with Lemmas again.

It quite a blow up of a code to add extra definition for each such lemma.

Vadim

CMU ECE PhD candidate

Mobile: +1(510)220-1060

[Coq-Club] obligations, Vadim Zaliva, 05/10/2016
- Re: [Coq-Club] obligations, Matthieu Sozeau, 05/10/2016
- Re: [Coq-Club] obligations, Daniel Schepler, 05/10/2016
  - Re: [Coq-Club] obligations, Vadim Zaliva, 05/10/2016
    - Re: [Coq-Club] obligations, Vadim Zaliva, 05/10/2016
      - Re: [Coq-Club] obligations, Matthieu Sozeau, 05/10/2016
        
        Re: [Coq-Club] obligations, Vadim Zaliva, 05/11/2016
        
        Re: [Coq-Club] obligations, Vadim Zaliva, 05/12/2016
        
        Re: [Coq-Club] obligations, Matthieu Sozeau, 05/12/2016