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

data Action

checkInternal traverses the whole Term, and we can use this traversal to modify the term.

Constructors

Action

Fields

• preAction :: Type -> Term -> TCM Term

  Called on each subterm before the checker runs.

• postAction :: Type -> Term -> TCM Term

  Called on each subterm after the type checking.

• relevanceAction :: Relevance -> Relevance -> Relevance

  Called for each ArgInfo. The first Relevance is from the type, the second from the term.

defaultAction :: Action

The default action is to not change the Term at all.

eraseUnusedAction :: Action

infer :: Term -> TCM Type

Infer type of a neutral term.

inferSort :: Term -> TCM Sort

Compute the sort of a type.