Ssreflect Users Discussion List

[Laurent Thery <>]

On 02/06/2016 11:54 AM, Felipe Cerqueira wrote:
> Let l := [:: 1; 2; 3].
>      Eval compute in (\sum_(x <- l) x).


Yep unfortunately for you the bigop operator is locked, in order to 
compute, you have to explicitly unlock it.

Lemma test: let: l := [:: 1; 2; 3] in \sum_(x <- l) x = 6)%N.
rewrite unlock.
compute.
by [].
Qed.