title: Interacting in agda-mode with agda?
body: <p>It feels <em>super awkward</em> to interact with agda.</p>
  <p>Consider the proof state:</p>
  <pre><code>_ = begin
    5 ∸ 3
    ≡⟨⟩
     4 ∸ 2 ≡⟨⟩
     3 ∸ 1 ≡⟨⟩
     2 ∸ 0 ≡⟨⟩  { 2 &lt;cursor-goes-here&gt; }0
  </code></pre>
  <p>When I type <code>C-c C-l</code> (<code>type-check</code>), it says</p>
  <pre><code>?0 : 2 ∸ 0 ≡ _y_131
  _y_131 : ℕ  [ at /home/bollu/work/plfa/src/plfa/part1/Naturals.lagda.md:586,5-10 ]
  </code></pre>
  <p>which doesn't seem like a great error? Nor does a <code>refine</code> (<code>C-c C-r</code>) give me a good error message: It only tells me:</p>
  <pre><code>cannot refine
  </code></pre>
  <ol>
  <li>How do I get adga to tell me:</li>
  </ol>
  <blockquote>
  <p>You've finished the proof, except for a missing <code>\qed</code></p>
  </blockquote>
  <ol start="2">
  <li>In general, what is the &quot;preferred mode of interaction&quot; when building proofs?</li>
  </ol>