title: How to do basic pattern matching with formal parameters (value binding) in Idris?
body: <p>When I try this in Idris,</p>
  
  <pre><code>contrived : (List a, Char, (Int, Double), String, Bool) -&gt; Bool
  contrived   ([]    ,  'b',  (1,   2.0),   "hi" , True) = False
  contrived    (a,  b,  c,   d,  e) = True
  </code></pre>
  
  <p>I receive the error message <code>Can't infer argument a to contrived, Can't infer argument a to List, Can't infer argument a to []</code>. But looking at the Manning book, I don't see any obvious syntactic issues with my approach.</p>