liquid-base-4.14.3.0: src/Data/Bits.spec

module spec Data.Bits where

//  TODO: cannot use this because `Bits` is not a `Num`
//  Data.Bits.shiftR :: (Data.Bits.Bits a) => x:a -> d:Nat 
//                   -> {v:a | ((d=1) => (x <= 2*v + 1 && 2*v <= x)) }