title: Is it possible to check the length of two strings before pattern matching against them?
body: <p>I'm programming in Coq and want to eliminate non-exhaustive case matching by checking the length of the  two strings first, for example</p>
  <pre class="lang-ml prettyprint-override"><code>Definition foo (word1 word2 : word) : option :=
      if length word1 =? length word2 then
      * pattern matching logic that only concerns same length word patterns *
      else None.
  </code></pre>
  <p>I still get a non-exhaustive pattern matching error. Is it possible for m to do this or do I have to approach my function in another way?</p>