Agda.TypeChecking.CheckInternal

A bidirectional type checker for internal syntax.

Performs checking on unreduced terms. With the exception that projection-like function applications have to be reduced since they break bidirectionality.

Documentation

checkType :: Type -> TCM ()

Entry point for e.g. checking WithFunctionType.

checkInternal :: Term -> Type -> TCM ()

Entry point for term checking.