coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Can you help with function in permutations.v?

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Can you help with function in permutations.v?
Date: Sat, 5 Jul 2014 16:35:59 +0300

Sorry, will push it soon.

On Sat, Jul 5, 2014 at 4:12 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Here it is:
https://github.com/zaarcis/linear_algebra_in_Coq/blob/master/permutations.v

I could not prove "Instance vect_perm_Proper" which I have put Admitted now.

I will be grateful for any hints.

Thanks,
Ilmars

[Coq-Club] Can you help with function in permutations.v?, Ilmārs Cīrulis, 07/05/2014
- Re: [Coq-Club] Can you help with function in permutations.v?, Ilmārs Cīrulis, 07/05/2014
  - Re: [Coq-Club] Can you help with function in permutations.v?, Ilmārs Cīrulis, 07/05/2014
    - Re: [Coq-Club] Can you help with function in permutations.v?, Ilmārs Cīrulis, 07/05/2014
      - Re: [Coq-Club] Can you help with function in permutations.v?, Ilmārs Cīrulis, 07/05/2014
        
        Re: [Coq-Club] Can you help with function in permutations.v?, Daniel Schepler, 07/05/2014
        
        Re: [Coq-Club] Can you help with function in permutations.v?, Ilmārs Cīrulis, 07/05/2014