function should be known in def (for general recursion)

diff --git a/Resolver.hs b/Resolver.hs
index d2d79aae7203a2c75be8f4235744f39fc7b1911d..30e9951540f18d40123a5f8257ff9338446eb6a3 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -297,7 +297,7 @@ resolveDecl d = case d of
   DeclDef (AIdent (_,f)) tele t body -> do
     let tele' = flattenTele tele
     a <- binds CTT.Pi tele' (resolveExp t)
-    d <- lams tele' (resolveWhere body)
+    d <- lams tele' (local (insertVar f) $ resolveWhere body)
     return ((f,(a,d)),[(f,Variable)])
   DeclData (AIdent (l,f)) tele sums -> do
     let tele' = flattenTele tele