Data.Digit.Decimal

record Dec 

MkDec : (toNat : Nat) -> (bound : So (lt toNat (fromInteger 10))) -> Dec

toNat : (rec : Dec) -> Nat

bound : (rec : Dec) -> So (lt (toNat rec) (fromInteger 10))

MkDec : (toNat : Nat) -> (bound : So (lt toNat (fromInteger 10))) -> Dec

mkDec : (d : Nat) -> {auto pr : So (lt d (fromInteger 10))} -> Dec

toChar : Dec -> Char