Ssreflect Users Discussion List

[Maxime Dénès <>]

Hello Vincent,

I guess the problem is that the row you defined has coefficients in 
bool, which is not equipped with a field structure (I think). The types 
look the same because of the notations hiding the types of coefficients, 
so a "Set Printing All" might be useful.

Cheers,
Maxime.

On 27/06/2011 14:03, Vincent Siles wrote:
> 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