| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 Term | Source

Type check an expression.
Produced by Haddock version 2.4.2