Some more docs for Data.Bits
commit791987306add2a78d343f3241efaea9e28328926
authorSynthetica9 <patrickhilhorst97@gmail.com>
dateFri 27 Jan 2017, 19:53 (10 years ago)
parenta3f8b0b
libs/base/Data/Bits.idr+2−1
@@ -72,7 +72,8 @@ data Bits : Nat -> Type where
7272 ||| up to the maximum supported by `machineTy`.
7373 MkBits : machineTy (nextBytes n) -> Bits n
7474
75−pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
75+||| Perform a function over Bits8 as if it is carried out on n bits
76+pad8 : (n : Nat) -> (f :(Bits8 -> Bits8 -> Bits8)) -> Bits8 -> Bits8 -> Bits8
7677pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
7778 where
7879 pad = getPad {n=0} n