diff options
| author | Enrico Tassi | 2015-03-09 11:07:53 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-03-09 11:24:38 +0100 |
| commit | fc84c27eac260dffd8f2fb1cb56d599f1e3486d9 (patch) | |
| tree | c16205f1637c80833a4c4598993c29fa0fd8c373 /mathcomp/ssrtest/testmx.v | |
Initial commit
Diffstat (limited to 'mathcomp/ssrtest/testmx.v')
| -rw-r--r-- | mathcomp/ssrtest/testmx.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/mathcomp/ssrtest/testmx.v b/mathcomp/ssrtest/testmx.v new file mode 100644 index 0000000..931cbad --- /dev/null +++ b/mathcomp/ssrtest/testmx.v @@ -0,0 +1,33 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat. +Require Import ssralg matrix. + +Set Implicit Arguments. +Unset Strict Implicit. +Import Prenex Implicits. + +Local Open Scope nat_scope. +Local Open Scope ring_scope. + +Section TestMx. + +Variable R : ringType. +Variable M : 'M[R]_2. + +Goal 1%:M = M. +Proof. +Set Printing All. +rewrite [(1%:M : 'M_(1+1)%N)]scalar_mx_block. +(* Success with 1.2 *) +(* With ssreflect 1.3, fails with error : *) +(* Toplevel input, characters 0-44: *) +(* Error: pattern (1%:M) does not match LHS of scalar_mx_block *) +Admitted. + +Goal 1%:M = M. +Proof. +rewrite [1%:M](scalar_mx_block 1%N 1%N). +(* Success in both ssr 1.2 and 1.3 *) +Admitted. + +End TestMx.
\ No newline at end of file |