title: Loading files in Agda: unclear explanation in Learn you an Agda
body: <p>I have made an emacs file <code>trial_agda.agda</code> with the following code:</p>
  
  <pre><code>module trial_agda where
  
  data  : Set where
    zero : 
    suc  :  → 
  
  data _even :  → Set where
    ZERO : zero even
    STEP : ∀ x → x even → suc (suc x) even
  
  _+_ :  →  → 
  (zero + n) = n
  (suc n) + n′ = suc (n + n′)
  </code></pre>
  
  <p>In <a href="http://learnyouanagda.liamoc.net/pages/proofs.html" rel="nofollow noreferrer">http://learnyouanagda.liamoc.net/pages/proofs.html</a>, the author writes:</p>
  
  <p><em>Now we’ll prove in Agda that four is even. Type the following into an emacs buffer, and type C-c C-l</em>:</p>
  
  <pre><code>-- \_1 to type ₁
  proof₁ : suc (suc (suc (suc zero))) even
  proof₁ = ?
  </code></pre>
  
  <p>I typed <code>C-c C-n</code> and then copied and pasted the above code. I received the error <code>Error: First load the file.</code> </p>
  
  <p>What has gone wrong?</p>