title: How to prove things about primitive strings?
body: <p>On Idris, it is not possible to perform pattern matching against primitive strings. As such, it is not obvious how to prove things about them. For example, this function may return a proof that the first character of a list of chars is 'a':</p>
  
  <pre><code>f : (l : List Char) -&gt; Maybe (head' l = Just 'a')
  f ('a' :: []) = Just Refl
  f xs          = Nothing
  </code></pre>
  
  <p>Which is pretty simple and passes the type checker. If we try to implement the same thing for native strings, though, we'll write something like this:</p>
  
  <pre><code>g : (s : String) -&gt; Maybe (prim__strHead s = 'a')
  g s = if prim__strHead s == 'a'
    then Just Refl 
    else Nothing
  </code></pre>
  
  <p>Which fails to typecheck because the compiler obviously can't conclude <code>prim__strHead s == 'a'</code> just from the fact it passed the <code>prim__strHead s == 'a'</code> test. </p>
  
  <p>What is, thus, the proper way to prove things about primitive strings?</p>