title: Do agda programs necessarily terminate?
body: <p>It has been stated a few places that all agda programs terminate.  However I can construct a function like this:</p>
  
  <pre><code>stall : ∀ n → ℕ
  stall 0 = 0
  stall x = stall x
  </code></pre>
  
  <p>The syntax highlighter doesn't seem to like it, but there are no compilation errors.</p>
  
  <p>Computing the normal form of <code>stall 0</code> results in <code>0</code>.  Computing the result of <code>stall 1</code> causes Emacs to hang in what looks a lot like a non-terminating loop.</p>
  
  <p>Is this a bug?  Or can Agda sometimes run forever?  Or is something more subtle going on?</p>