ModuleAgda-2.7.0.1Haskell2010

Agda.TheTypeChecker

valuecheckDecls :: [Declaration] -> TCM ()

Type check a sequence of declarations.

valuecheckDecl :: Declaration -> TCM ()

Type check a single declaration.

valuecheckDeclCached :: Declaration -> TCM ()

Cached checkDecl

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

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

valuecheckExpr :: Expr -> Type -> TCM Term

Type check an expression.