diff options
| author | Kazuhiko Sakaguchi | 2018-07-12 20:19:55 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2018-07-12 20:19:55 +0900 |
| commit | 10171942883948c8144ec076ef48eb73f8e49cdd (patch) | |
| tree | e5e5f5ff58fd3b3c07afd49388afcab5cbbe165b /mathcomp/algebra/matrix.v | |
| parent | b8be28130d6a2a057858e3978c75ee0796630dce (diff) | |
Replace all the CoInductives with Variants
Diffstat (limited to 'mathcomp/algebra/matrix.v')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index ec9fcc5..fca25a9 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -870,7 +870,7 @@ Proof. by rewrite card_prod !card_ord. Qed. Definition mxvec_index (i : 'I_m) (j : 'I_n) := cast_ord mxvec_cast (enum_rank (i, j)). -CoInductive is_mxvec_index : 'I_(m * n) -> Type := +Variant is_mxvec_index : 'I_(m * n) -> Type := IsMxvecIndex i j : is_mxvec_index (mxvec_index i j). Lemma mxvec_indexP k : is_mxvec_index k. |