Idris2Doc : Data.Bytes.Proofs

Data.Bytes.Proofs

(source)
Definitions
data IsMultN : Nat -> Nat -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
ZeroN : IsMultN {_:4792} 0
  
PlusN : IsMultN n m -> IsMultN n (plus n m)
isMultN : (n : Nat) -> (m : Nat) -> Maybe (IsMultN n m)
  Totality: total
  Visibility: public export
viewMultN : (0 n : Nat) -> (0 m : Nat) -> IsMultN n m -> (x : Nat ** m = x * n)
  Totality: total
  Visibility: public export
byteToBits : Fin byteSize -> Fin (byteSize * 8)
  Totality: total
  Visibility: export