Add a test for nested where-clauses calling outer where-clause

agda · Sep 18, 2024 · 13ccde1 · 13ccde1
1 parent 528a7f2
commit 13ccde1
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/test/Where.agda b/test/Where.agda
@@ -51,14 +51,16 @@ ex4 b = mult 42
 ex4' : Bool → Nat
 ex4' b = mult (bool2nat b)
   where
+    extra : Nat
+    extra = 14
     mult : Nat → Nat
     mult n = bump n (bool2nat b)
       where
         bump : Nat → Nat → Nat
         bump x y = go (x * y) (n - bool2nat b)
           where
             go : Nat → Nat → Nat
-            go z w = z + x + w + y + n + bool2nat b
+            go z w = z + x + w + y + n + bool2nat b + extra
 
 -- with pattern matching and multiple clauses
 ex5 : List Nat → Nat

diff --git a/test/golden/Where.hs b/test/golden/Where.hs
@@ -44,14 +44,16 @@ ex4 b = mult 42
 ex4' :: Bool -> Natural
 ex4' b = mult (bool2nat b)
   where
+    extra :: Natural
+    extra = 14
     mult :: Natural -> Natural
     mult n = bump n (bool2nat b)
       where
         bump :: Natural -> Natural -> Natural
         bump x y = go (x * y) (n - bool2nat b)
           where
             go :: Natural -> Natural -> Natural
-            go z w = z + x + w + y + n + bool2nat b
+            go z w = z + x + w + y + n + bool2nat b + extra
 
 ex5 :: [Natural] -> Natural
 ex5 [] = zro