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

Safe Haskell	None
Language	Haskell2010

Agda.TheTypeChecker

Synopsis

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

Documentation

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

Type check a sequence of declarations.

checkDecl :: Declaration -> TCM () Source #

Type check a single declaration.

checkDeclCached :: Declaration -> TCM () Source #

Cached checkDecl

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

Infer the type of an expression. Implemented by checking against a meta variable. Except for neutrals, for them a polymorphic type is inferred.

checkExpr :: Expr -> Type -> TCM Term Source #

Type check an expression.