ModuleAgda-2.8.0.2Haskell2010

Agda.TheTypeChecker

Synopsis

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.