[Agda] Set levels and library issues

[Matthew]

Hello Agda-ers,

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.

Any pointers gratefully received.  I've also a general question about 
library versions, see end of this message.  Thanks!

open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec as Vec using (Vec; _?_; [])

test0 : Vec {?} N 2
test0 = 1 ? 2 ? []

-- C-c C-a is very useful...
-- ...but it provided a term  {.Level.suc .Level.zero} for the Goal 
below which does not typecheck
test1 : Vec {?} Set 2
test1 = (Fin 1) ? (Fin 2) ? []

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?

-- 
Title of html document Matthew Fairtlough

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121128/644e3106/attachment.html