Decimal.agda

module Decimal where
open import Data.Nat

infixr 5 _∷_
infixl 8 _^_

_^_ : ℕ → ℕ → ℕ
n ^ zero = 1
n ^ (suc m) = n * (n ^ m)

data Decimal : ℕ → ℕ → Set where
  [_] : (n : ℕ) → Decimal 1 n
  _∷_ : ∀ {place val} → (n : ℕ) → Decimal place val → Decimal (suc place) (n * 10 ^ place + val)

decimal-7 : Decimal 1 7
decimal-7 = [ 7 ]

-- invalid-decimal-7 : Decimal 4 7
-- invalid-decimal-7 = [ 7 ]

decimal-648 : Decimal 3 648
decimal-648 = 6 ∷ 4 ∷ [ 8 ]

-- invalid-decimal-648 : Decimal 3 99
-- invalid-decimal-648 = 6 ∷ 4 ∷ [ 8 ]

decimal-021 : Decimal 3 21
decimal-021 = 0 ∷ 2 ∷ [ 1 ]