summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Rules/Term.hs-boot
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Rules/Term.hs-boot')
-rw-r--r--src/full/Agda/TypeChecking/Rules/Term.hs-boot6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/full/Agda/TypeChecking/Rules/Term.hs-boot b/src/full/Agda/TypeChecking/Rules/Term.hs-boot
index f166ac3..501ecc3 100644
--- a/src/full/Agda/TypeChecking/Rules/Term.hs-boot
+++ b/src/full/Agda/TypeChecking/Rules/Term.hs-boot
@@ -1,9 +1,9 @@
module Agda.TypeChecking.Rules.Term where
+import Agda.Syntax.Common (WithHiding)
import qualified Agda.Syntax.Abstract as A
-import Agda.Syntax.Internal
--- import Agda.Syntax.Common hiding (Arg, Dom, NamedArg)
+import Agda.Syntax.Internal as I
import Agda.Syntax.Position
import Agda.TypeChecking.Monad.Base
import Agda.Utils.Except ( ExceptT )
@@ -17,3 +17,5 @@ checkArguments :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg A.Expr]
checkArguments' :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg A.Expr] -> Type -> Type ->
(Args -> Type -> TCM Term) -> TCM Term
+
+checkPostponedLambda :: I.Arg ([WithHiding Name], Maybe Type) -> A.Expr -> Type -> TCM Term