6
6
-- import Agda.Syntax.Common hiding (Arg, Dom, NamedArg)
7
7
import Agda.Syntax.Position
8
8
import Agda.TypeChecking.Monad.Base
11
11
isType_ :: A.Expr -> TCM Type
13
13
checkExpr :: A.Expr -> Type -> TCM Term
15
15
checkArguments :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg A.Expr] -> Type -> Type ->
16
ErrorT (Args, [NamedArg A.Expr], Type) TCM (Args, Type)
16
ExceptT (Args, [NamedArg A.Expr], Type) TCM (Args, Type)
18
18
checkArguments' :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg A.Expr] -> Type -> Type ->
19
19
(Args -> Type -> TCM Term) -> TCM Term