Idris2Doc : Data.Binary.Digit

Data.Binary.Digit

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