title: Typed Racket: Natural Numbers
body: <p>I have to solve a problem with a unique definition of the natural numbers:</p>
  
  <pre><code>(define-type Nat (U 'Zero Succ))
  (define-struct Succ ([prev : Nat]) #:transparent)
  </code></pre>
  
  <p>So basically, <code>0 = 'Zero, 1 = (Succ 'Zero), 2 = (Succ (Succ 'Zero))....</code> etc.</p>
  
  <p>Using this form, without converting them into integers, I have write recursive functions to add, subtract, and multiply the natural numbers. For the add function I've tried this</p>
  
  <pre><code>(: nat+ : Nat Nat -&gt; Nat)
  (define (nat+ n m)
    (match '(n m)
      ['('Zero 'Zero) 'Zero]
      ['((Succ p) 'Zero)
       n]
      ['('Zero (Succ p))
       m]
      ['((Succ p) (Succ t))
       (nat+ p (Succ m))]))
  </code></pre>
  
  <p>but I get the error </p>
  
  <blockquote>
    <p>p: unbound identifier in module in: p.</p>
  </blockquote>
  
  <p>Does anyone have any advice for writing this type of recursive function.</p>