Agda-2.2.10: 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.6.1