Skip to content

Commit

Permalink
Replace deprecated functions.
Browse files Browse the repository at this point in the history
  • Loading branch information
ReilySiegel committed Sep 4, 2024
1 parent 3be2e17 commit 93cc5fd
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Utils/Bytes.idr
Original file line number Diff line number Diff line change
Expand Up @@ -140,9 +140,9 @@ shiftR' x i = maybe_a_a zeroBits $ do
export
rotl : FiniteBits a => {n : Nat} -> {auto prf : ((S n) = bitSize {a})} -> Fin (S n) -> a -> a
rotl FZ x = x
rotl (FS i) x = (shiftL x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftR x $ bitsToIndex $ invFin $ coerce prf $ weaken i)
rotl (FS i) x = (shiftL x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftR x $ bitsToIndex $ complement $ coerce prf $ weaken i)

export
rotr : FiniteBits a => {n : Nat} -> {auto prf : ((S n) = bitSize {a})} -> Fin (S n) -> a -> a
rotr FZ x = x
rotr (FS i) x = (shiftR x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftL x $ bitsToIndex $ invFin $ coerce prf $ weaken i)
rotr (FS i) x = (shiftR x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftL x $ bitsToIndex $ complement $ coerce prf $ weaken i)

0 comments on commit 93cc5fd

Please sign in to comment.