Ssreflect Users Discussion List

["John Wiegley" <>]

Hello,

Perhaps this feature already exists, but something I would find useful are
length-predicated sequences: namely, a generalization of both non-empty lists
and lists of fixed size.  I see that we have mkseq for the latter, but I could
not find the former, and at any rate the generalization would allow for
non-empty length-bounded lists, etc.

Thank you,
  John