Ssreflect Users Discussion List

[Georges Gonthier <>]

  Indeed, the definition is missing the %:R cast. Of course, you would have 
avoided that error by using the relevant construct provided by the matrix 
library, namely delta_mx 0 0.

  Cheers,
Georges

-----Original Message-----
From: Maxime Dénès [] 
Sent: 27 June 2011 13:11
To: 
Subject: Re: how to debug hidden implicits

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