<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? 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. I've also a general question
about library versions, see end of this message. 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; _∷_; [])<br>
<br>
test0 : Vec {?} ℕ 2<br>
test0 = 1 ∷ 2 ∷ []<br>
<br>
-- C-c C-a is very useful...<br>
-- ...but it provided a term {.Level.suc .Level.zero} for the Goal
below which does not typecheck<br>
test1 : Vec {?} Set 2<br>
test1 = (Fin 1) ∷ (Fin 2) ∷ []<br>
<br>
I'm using Agda2.3.2 and the development library BTW. 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. Since I just installed Agda, it's my only obvious
choice as the standard library is not supposed to work with 2.3. 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>