module Test where
import Clash.Prelude

-- this just puts zeros in front of the bit vector
f :: KnownNat a => BitVector a -> BitVector (a + 1)
f bv = zeroExtend bv

-- this gets the length of a bit vector, as an SNat
g :: KnownNat a => BitVector a -> SNat a
g _ = SNat

-- this gets the length of *any* 'thing with known size that can become
-- a bitvector'
h :: (BitPack a, BitSize a ~ n, KnownNat n) => a -> SNat n
h _ = SNat