nat-test.egi

(define $Nat
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     [$inductive-match
      (deconstructor
        {[o []
          {[<o> {[]}]                   
           [_ {}]
           }]
         [s [Nat]
          {[<s $x> {x}]
           [_ {}]
           }]
         })]
     [$equal?
      (lambda [$val $tgt]
        (match [val tgt] [Nat Nat]
          {[[<o> <o>] <true>]
           [[<s $n1> <s $n2>] (= n1 n2)]
           [[_ _] <false>]}))]
     }))

(define $+
  (lambda [$m $n]
    (match m Nat
      {[<o> n]
       [<s $m1> <s (+ m1 n)>]})))

(define $*
  (lambda [$m $n]
    (match m Nat
      {[<o> <o>]
       [<s <o>> n]
       [<s $m1> (+ n (* m1 n))]})))
                  
(define $fact
  (lambda [$n]
    (match n Nat
      {[<o> <s <o>>]
       [<s $n1> (* n (fact n1))]})))

(test (fact <s <s <s <o>>>>))

(define $fib
  (lambda [$n]
    (match n Nat
      {[<o> <s <o>>]
       [<s <o>> <s <o>>]
       [<s <s $n1>> (+ (fib <s n1>) (fib n1))]})))

(test (fib <s <s <s <s <s <s <o>>>>>>>))

(define $monus
  (lambda [$m $n]
    (match [m n] [Nat Nat]
      {[[_ <o>] m]
       [[<o> _] <o>]
       [[<s $m1> <s $n1>] (monus m1 n1)]})))

(test (monus <s <s <o>>> <s <o>>))

(define $mod
  (lambda [$m $n]
    (match (monus m n) Nat
      {[<o> m]
       [$m1 (mod m1 n)]})))

(test (mod <s <s <s <s <o>>>>> <s <s <s <o>>>>))