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

Safe HaskellSafe-Infered

Agda.TypeChecker

Synopsis

Documentation

checkDecls :: [Declaration] -> TCM ()Source

Type check a sequence of declarations.

checkDecl :: Declaration -> TCM ()Source

Type check a single declaration.

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

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

checkExpr :: Expr -> Type -> TCM TermSource

Type check an expression.