title: Pattern matching on Type in Idris
body: <p>Probably it's elementary but I don't understand why the following function answers 1 for <strong>fnc Nat</strong> and also, for <strong>fnc Integer</strong>, which is not even included as a pattern.</p>
  
  <pre><code>fnc : Type -&gt; Integer
  fnc Bool = 1
  fnc Nat = 2
  </code></pre>