Skip to content

Commit

Permalink
Removing unnecessary code.
Browse files Browse the repository at this point in the history
  • Loading branch information
Matthew-Mosior committed Nov 19, 2024
1 parent b09b632 commit cc029f7
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions src/Data/RRBVector/Internal.idr
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ bitSizeOf ty = bitSize {a = ty}

public export
Shift : Type
Shift = Nat--Integer
Shift = Nat

||| The number of bits used per level.
export
Expand All @@ -40,7 +40,7 @@ blockshift = 4
||| The maximum size of a block.
export
blocksize : Nat
blocksize = integerToNat $ 1 `shiftL` blockshift--(integerToNat blockshift)
blocksize = integerToNat $ 1 `shiftL` blockshift

||| The mask used to extract the index into the array.
export
Expand All @@ -58,7 +58,6 @@ down sh = minus sh blockshift
export
radixIndex : Nat -> Shift -> Nat
radixIndex i sh = integerToNat ((natToInteger i) `shiftR` sh .&. (natToInteger blockmask))
-- the Nat (cast ((the Integer (cast $ shiftR i sh)) .&. (the Integer (cast blockmask))))

partial
export
Expand Down

0 comments on commit cc029f7

Please sign in to comment.