coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] obligations

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] obligations
Date: Tue, 10 May 2016 16:32:34 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f48.google.com
Ironport-phdr: 9a23:YwraSh1B9fmeDAuDsmDT+DRfVm0co7zxezQtwd8ZsegVIvad9pjvdHbS+e9qxAeQG96LurQd16GP6/iocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC3oLui6vro8WbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSJDUgKWE8osPx5jfZSg7aw3IATmUXnwcAOA/X4RjnFsP0uzfmv+9V3SCGIcTzC7cuVmLxvO9QVBb0hXJfZHYC+2bNh5kogQ==

Hi,

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 := _.

Cheers,

-- Matthieu

On Tue, May 10, 2016 at 6:18 PM Vadim Zaliva <vzaliva AT cmu.edu> wrote:

On Mon, May 9, 2016 at 6:12 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:
Any suggestions?

I have filed a bug for this but I am looking for a workaround other than switching
back to 8.4 :(

https://coq.inria.fr/bugs/show_bug.cgi?id=4723

--
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