title: Coq dependent types
body: <p>I am new to Coq and need some help with some of trivial examples to get me started. In particular I am interested in defining some operations of vectors (fixed size lists) using dependent types. I started with Vector package and trying to implement some additional  functions. For example I am having difficulty implementing trivial 'take' and 'drop' functions, which take or drop first 'p' elements from the list.</p>
  
  <pre><code>Require Import Vector.
  
  Fixpoint take {A} {n} (p:nat) (a: t A n) : p&lt;=n -&gt; t A p := 
     match a return ( p&lt;=n -&gt; t A p) with
       | cons A v (S m) =&gt; cons (hd v) (take m (tl v)) m
       | nil =&gt; fun pf =&gt; a
     end.
  </code></pre>
  
  <p>The error (in case of <code>nil</code>) is:</p>
  
  <pre><code>The term "a" has type "t A n" while it is expected to have type "t A p".
  </code></pre>
  
  <p>Could somebody help me with some starting points? Thanks!</p>