enumFromThenTo package:sbv

enumFromThenTo m n. Symbolic version of [m, m' .. n]

Constructing [x, y, .. z] and [x .. y]. Only works when all arguments are concrete and integral and the result is guaranteed finite Note that the it isn't "obviously" clear why the following works; after all we're doing the construction over Integer's and mapping it back to other types such as SIntN/SWordN. The reason is that the values we receive are guaranteed to be in their domains; and thus the lifting to Integers preserves the bounds; and then going back is just fine. So, things like [1, 5 .. 200] :: [SInt8] work just fine (end evaluate to empty list), since we see [1, 5 .. -56] in the Integer domain. Also note the explicit check for s /= f below to make sure we don't stutter and produce an infinite list.