<html>
  <head>
    <meta content="text/html; charset=ISO-8859-1"
      http-equiv="Content-Type">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    Hello Agda-ers,<br>
    <br>
    I'm newly using Agda for some investigations into heterogeneous
    vectors (a kind of extended sum type) and I wonder if anyone could
    point me to documentation about .Level's?&nbsp; I'm interested to know,
    for instance, what the inferred arguments of the (development
    library) vector type constructor Vec are in the two examples below.<br>
    <br>
    Any pointers gratefully received.&nbsp; I've also a general question
    about library versions, see end of this message.&nbsp; Thanks!<br>
    <br>
    open import Data.Nat<br>
    open import Data.Fin using (Fin; zero; suc)<br>
    open import Data.Vec as Vec using (Vec; _&#8759;_; [])<br>
    <br>
    test0 : Vec {?} &#8469; 2<br>
    test0 = 1 &#8759; 2 &#8759; []<br>
    <br>
    -- C-c C-a is very useful...<br>
    -- ...but it provided a term&nbsp; {.Level.suc .Level.zero} for the Goal
    below which does not typecheck<br>
    test1 : Vec {?} Set 2<br>
    test1 = (Fin 1) &#8759; (Fin 2) &#8759; []<br>
    &nbsp;<br>
    I'm using Agda2.3.2 and the development library BTW.&nbsp; It seems to
    compile ok though the documentation warns me that I may need to use
    the development version of Agda to use the development version of
    the library.&nbsp; Since I just installed Agda, it's my only obvious
    choice as the standard library is not supposed to work with 2.3.&nbsp; Is
    there a timeline for a library version which is known to work out of
    the box with the latest release of Agda?<br>
    <br>
    <div class="moz-signature">-- <br>
      <meta http-equiv="Content-Type" content="text/html;
        charset=ISO-8859-1">
      <title>Title of html document</title>
      <link rel="stylesheet" href="styles.css" type="text/css">
      Matthew Fairtlough<br>
      <br>
    </div>
  </body>
</html>