Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.CheckInternal
Description
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
checkInternal :: Term -> Type -> TCM () #
Entry point for term checking.
defaultAction :: Action #