summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Rules/Def.hs-boot
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Rules/Def.hs-boot')
-rw-r--r--src/full/Agda/TypeChecking/Rules/Def.hs-boot4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/full/Agda/TypeChecking/Rules/Def.hs-boot b/src/full/Agda/TypeChecking/Rules/Def.hs-boot
index b7721a4..7dbeb2d 100644
--- a/src/full/Agda/TypeChecking/Rules/Def.hs-boot
+++ b/src/full/Agda/TypeChecking/Rules/Def.hs-boot
@@ -1,6 +1,6 @@
module Agda.TypeChecking.Rules.Def where
-import Agda.Syntax.Abstract
+import Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.TypeChecking.Monad
@@ -10,4 +10,6 @@ checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
checkFunDef' :: I.Type -> ArgInfo -> Delayed -> Maybe ExtLamInfo -> Maybe QName -> DefInfo -> QName -> [Clause] -> TCM ()
+newSection :: ModuleName -> A.Telescope -> TCM a -> TCM a
+
useTerPragma :: Definition -> TCM Definition