!import "base.tri" !Local
!import "list.tri" !Local

pred = y (self : triage
  0
  (_ : 0)
  (bit rest :
    matchBool
      -- odd: 2n + 1 -> 2n
      (matchBool
        0
        (pair 0 rest)
        (equal? rest 0))
      -- even: 2n -> 2n - 1
      (matchBool
        0
        (pair 1 (self rest))
        (equal? rest 0))
      bit))

incDecRev = y (self : matchList
  "1"
  (digit rest :
    matchBool
      (pair 48 (self rest))
      (pair (succ digit) rest)
      (equal? digit 57)))

showNumberRev_ = y (self n acc :
  matchBool
    acc
    (self (pred n) (incDecRev acc))
    (equal? n 0))

showNumber = (n :
  matchBool
    "0"
    (reverse (showNumberRev_ n t))
    (equal? n 0))