title: How to understand the type declaration and definition for List and Vect in Idris lang?
body: <p>In <a href="http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#list-and-vect" rel="nofollow noreferrer">Idris doc</a> there are the following lines:</p>
  
  <pre><code>data List a = Nil | (::) a (List a)
  
  data Vect : Nat -&gt; Type -&gt; Type where
     Nil  : Vect Z a
     (::) : a -&gt; Vect k a -&gt; Vect (S k) a
  </code></pre>
  
  <p>I assumed line 1 is a type definition for List and the rest is type declaration for Vect.
  I thought there should be both declaration and definition so I looked in the <a href="https://github.com/idris-lang/Idris-dev" rel="nofollow noreferrer">Idris repo</a> and found:</p>
  
  <pre><code>data List : (elem : Type) -&gt; Type where
    Nil : List elem
    (::) : (x : elem) -&gt; (xs : List elem) -&gt; List elem
  </code></pre>
  
  <p>Which shares a similar pattern with type declaration of Vect so it seems fine. but I cannot find <code>data List a = Nil | (::) a (List a)</code> in souce code. Also, I cannot find type definition for Vect.</p>
  
  <p>So, my confusions are:</p>
  
  <ul>
  <li>Why I can't find <code>data List a = Nil | (::) a (List a)</code> in source code?</li>
  <li>What's the actual type definition for Vect?</li>
  </ul>