Skip to Content.

Sympa Menu

coq-club - [Coq-Club] Can you help with function in permutations.v?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Can you help with function in permutations.v?
Date: Sat, 5 Jul 2014 16:12:41 +0300

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

Archive powered by MHonArc 2.6.18.