title: How does one read the syntax for the Braun tree insertion?
body: <p>In the section on insertion into Braun trees of the <a href="https://svn.divms.uiowa.edu/repos/clc/projects/agda/book/book.pdf" rel="nofollow noreferrer">Verified Programming in Agda book</a> (page 118), the author does some explanation of what the code is supposed to be doing, but leaving what it does aside, a singificant ommision in the book so far is not explaining the strange syntax in function pattern matching for theorem proving.</p>
  
  <p>I understand that the <a href="http://agda.readthedocs.io/en/latest/language/with-abstraction.html" rel="nofollow noreferrer">with pattern</a> can be further destructured by using <code>|</code> and I can understand that when using <code>rewrite</code>, <code>|</code> can also be used to separate the different rewrites, but this makes it confusing.</p>
  
  <p>As far as I can tell, rewrite is definitely not a function. And then comes the following:</p>
  
  <pre><code>bt-insert a (bt-node{n}{m} a' l r p) 
    rewrite +comm n m with p | if a &lt;A a' then (a , a') else (a' , a)
  bt-insert a (bt-node{n}{m} a' l r _) | inj₁ p | (a1 , a2) 
    rewrite p = (bt-node a1 (bt-insert a2 r) l (inj₂ refl))
  bt-insert a (bt-node{n}{m} a' l r _) | inj₂ p | (a1 , a2) = 
    (bt-node a1 (bt-insert a2 r) l (inj₁ (sym p)))
  </code></pre>
  
  <p>I am really confused as to how <code>rewrite +comm n m with p | if a &lt;A a' then (a , a') else (a' , a)</code> should be parsed mentally. And how does one read <code>| inj₁ p | (a1 , a2)  rewrite p</code>? Also, while testing the previous examples I've discovered that for some reason the order of the rewrites does not matter. Why is that?</p>