[Agda] Set levels and library issues

[Nils Anders Danielsson]

On 2012-11-28 11:48, Matthew wrote:
> 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.

Make sure that the level names are in scope (open import Level) and type
"C-c C-s" to fill in any solved meta-variables.

> Is there a timeline for a library version which is known to work out
> of the box with the latest release of Agda?

There is none. I hope to release a new version of the library fairly
soon.

-- 
/NAD