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

(test ((type-ref Nat =) <o> <o>))

(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 $val-match-test
  (lambda [$n]
    (match n Nat
      {[,(+ <s <o>> <s <s <o>>>) <ok>]
       [$n1 n1]})))

(test (val-match-test <s <s <s <o>>>>))

(define $on-pat-test
  (lambda [$m $n]
    (match [m n] [Nat Nat]
      {[[$m1 (on [$m1] <s m1>)] m1]
       [[_ _] <not-ok>]})))

(test (on-pat-test <o> <s <o>>))

(define $on-pat-test2
  (lambda [$m $n]
    (match [m n] [Nat Nat]
      {[[$m1 <s (on [$m1] m1)>] m1]
       [[_ _] <not-ok>]})))

(test (on-pat-test2 <o> <s <o>>))