eof package:Agda

True if we are at the end of the file.
Confluence checking incomplete because the definition of the QName contains unsolved metavariables.
This type, representing a type of sizes, might be empty.
Get type of a constant, instantiated to the current context.
Check that the main function has type IO a, for some a.
Pretty-prints the type of the meta-variable.