
  0 | module Huffman.Fin256
  1 | 
  2 | import Data.Fin
  3 | import Data.Bits
  4 | 
  5 | public export
  6 | bits8ToFin256 : Bits8 -> Fin 256
  7 | bits8ToFin256 i =
  8 |     case natToFin (cast i) 256 of
  9 |         Just x => x
 10 |         Nothing => assert_total $ idris_crash "can't happen"
 11 | 
 12 |