0 | module Data.Binary.Digit
 1 |
 2 | %default total
 3 |
 4 | ||| This is essentially Bool but with names that are easier
 5 | ||| to understand
 6 | public export
 7 | data Digit : Type where
 8 |   O : Digit
 9 |   I : Digit
10 |
11 | ||| Translation to Bool
12 | public export
13 | isI : Digit -> Bool
14 | isI I = True
15 | isI O = False
16 |
17 | public export
18 | toNat : Digit -> Nat
19 | toNat O = 0
20 | toNat I = 1
21 |