Idris2Doc : Data.Binary.Digit

Data.Binary.Digit

Definitions

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

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

Totality: total
Visibility: public export
toNat : Digit -> Nat
Totality: total
Visibility: public export