Ssreflect Users Discussion List

[Vincent Siles <>]

Hi list,
still playing with matrices and I want to define the row matrix which
starts with 1 then 0 everywhere else.

Section Foo.
Variable F : fieldType.

Definition row10 (n:nat)  : 'rV[F]_(1+n) :=
\row_(j < 1 + n) (j == 0).

End Foo.

This piece of code raise the following error

Toplevel input, characters 65-90:
Error: In environment
R : fieldType
n : nat
The term "\row_j (j == 0)" has type "'rV_(1 + n)"
 while it is expected to have type "'rV_(1 + n)".


If I omit the type of row10, the definition is accepted, and is
given the exact same type.

I guess there are some "hidden magic" happening, but why does ssreflect reject
the first definition ?


Cheers,
Vincent