ssreflect - defining an executable version of rank

Subject: Ssreflect Users Discussion List

List archive

defining an executable version of rank

From: Vincent Siles <>
To:
Subject: defining an executable version of rank
Date: Tue, 21 Jun 2011 14:31:01 +0200

I have defined a function to effectively compute the rank of matrix and
want to prove it correct in ssr. Is the only way to prove is to prove that is
something like

forall n m (A : 'M[R]_(n,m)), \rank A = my_rank n m A

?

Cheers,
Vincent

defining an executable version of rank, Vincent Siles, 06/21/2011
- RE: defining an executable version of rank, Georges Gonthier, 06/21/2011
  - Re: defining an executable version of rank, Vincent Siles, 06/21/2011
    - RE: defining an executable version of rank, Georges Gonthier, 06/21/2011

List archive

defining an executable version of rank