Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecker

Synopsis

- checkDecls :: [Declaration] -> TCM ()
- checkDecl :: Declaration -> TCM ()
- inferExpr :: Expr -> TCM (Term, Type)
- checkExpr :: Expr -> Type -> TCM Term

# Documentation

checkDecls :: [Declaration] -> TCM ()

Type check a sequence of declarations.

checkDecl :: Declaration -> TCM ()

Type check a single declaration.

inferExpr :: Expr -> TCM (Term, Type)

Infer the type of an expression. Implemented by checking agains a meta variable.

checkExpr :: Expr -> Type -> TCM Term

Type check an expression.