[Agda] Set levels and library issues

Nils Anders Danielsson nad at chalmers.se
Wed Nov 28 16:06:06 CET 2012

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


More information about the Agda mailing list