From: Simon Huber <hubsim@gmail.com>
Date: Wed, 8 Apr 2015 14:41:04 +0000 (+0200)
Subject: function should be known in def (for general recursion)
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=01aff1cb9542fa6b51efd760a25f6850f19e2a69;p=cubicaltt.git

function should be known in def (for general recursion)
---

diff --git a/Resolver.hs b/Resolver.hs
index d2d79aa..30e9951 100644
--- 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