Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecker
Synopsis
checkDecls :: [Declaration] -> TCM ()
checkDecl :: 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.
inferExpr :: Expr -> TCM (Term, Type)Source
Infer the type of an expression. Implemented by checking agains a meta variable.
checkExpr :: Expr -> Type -> TCM TermSource
Type check an expression.
Produced by Haddock version 2.6.1