The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Okay, it's here now.

Apologies, it's obvious now that I'm too ill for anything that needs thinking.

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

Okay, it's here. I forgot to change mail again, hope the friend will not complain.

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

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