Idris2Doc : Data.Binary.Digit

Data.Binary.Digit

data Digit : Type
  This is essentially Bool but with names that are easier
  to understand

  Totality: total
  Constructors:
  
O : Digit
  
I : Digit
isI : Digit -> Bool
  Translation to Bool

  Totality: total
toNat : Digit -> Nat
  Totality: total