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.

checkInternal' :: Action -> Term -> Type -> TCM Term

defaultAction :: Action

data Action

Constructors

Action

Fields

preAction :: Type -> Term -> TCM Term

postAction :: Type -> Term -> TCM Term

infer :: Term -> TCM Type

Infer type of a neutral term.