Ssreflect Users Discussion List

[bertot <>]

We all know the problem, but it may be interesting to record it in 
written form.

 l : seq bigQ
  k : nat
  ============================
   (size l == 0)%B -> ...


rewrite size_eq0.  provokes the following error

Toplevel input, characters 0-16:
Error: The LHS of size_eq0
    (size _ == 0)%B
does not match any subterm of the goal

The error message should help users understand that
size l == 0 does not match because bigQ  is not an EqType.

How shall we do that?