Closed kleinreact closed 1 month ago
Shifting a bit into a 0-length BitVector with (+>>.) or (.<<+) currently fails with an out of range exception.
(+>>.)
(.<<+)
We should either define the operations to keep empty bit vectors unchanged or exclude them from the interface via adding some 1 <= n constraints.
1 <= n
The former would be the way to go in order to stay consistent with (+>>) and (<<+):
(+>>)
(<<+)
clashi> high +>> (Nil :: Vec 0 Bit) Nil clashi> (Nil :: Vec 0 Bit) <<+ low Nil
Shifting a bit into a 0-length BitVector with
(+>>.)
or(.<<+)
currently fails with an out of range exception.We should either define the operations to keep empty bit vectors unchanged or exclude them from the interface via adding some
1 <= n
constraints.The former would be the way to go in order to stay consistent with
(+>>)
and(<<+)
: