Ssreflect Users Discussion List

[sidi <>]

Hi Thomas,

In your example to get P.[4] you can use the Lemma coef_Poly. For every poly constructor (in your case constructor from a sequence) you should have rewriting lemma u  can use instead of the unfold and unlock.

Regards.

On Wed, Mar 28, 2012 at 2:09 PM, Thomas Sibut-Pinote <> wrote:

Hi,
I have noticed that most computations are blocked in ssreflect, and that sometimes I can trick them into calculating using "rewrite /<name_of_the_function> unlock".
However, I just started using polynomials, and I can't get them to evaluate at a point, or get the leading coefficient.


Definition P :=  (Poly  ( [:: 1%:Z; 3%:Z; 1%:Z; 3%:Z])).
Eval compute in (P.[4]).
Eval compute in (lead_coef P).

Thank you in advance !
Thomas

--
Sidi