From 2f69f2a001f08050724fd2bee7590ae10c3f91c3 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Thu, 22 Feb 2024 16:22:06 +0100
Subject: [PATCH] [ clean ] remove underLambdas and underAbs

---
 src/full/Agda/TypeChecking/RecordPatterns.hs  |  2 --
 .../Agda/TypeChecking/Substitute/Class.hs     | 22 -------------------
 2 files changed, 24 deletions(-)

diff --git a/src/full/Agda/TypeChecking/RecordPatterns.hs b/src/full/Agda/TypeChecking/RecordPatterns.hs
index cf2af61c499..0555a0594c9 100644
--- a/src/full/Agda/TypeChecking/RecordPatterns.hs
+++ b/src/full/Agda/TypeChecking/RecordPatterns.hs
@@ -371,8 +371,6 @@ recordExpressionsToCopatterns = \case
 --              -- go from level (i + n - 1) to index (subtract from |xs|-1)
 --              index             = length xs - (i + n)
 --          in  Done xs' $ applySubst (liftS (length xs2) $ us ++# raiseS 1) v
---          -- The body is NOT guarded by lambdas!
---          -- WRONG: underLambdas i (flip apply) (map defaultArg us) v
 --
 --        Fail -> Fail
 --
diff --git a/src/full/Agda/TypeChecking/Substitute/Class.hs b/src/full/Agda/TypeChecking/Substitute/Class.hs
index dd80d7c898d..50f88104bd9 100644
--- a/src/full/Agda/TypeChecking/Substitute/Class.hs
+++ b/src/full/Agda/TypeChecking/Substitute/Class.hs
@@ -326,25 +326,3 @@ mkAbs x v | 0 `freeIn` v = Abs x v
 reAbs :: (Subst a, Free a) => Abs a -> Abs a
 reAbs (NoAbs x v) = NoAbs x v
 reAbs (Abs x v)   = mkAbs x v
-
--- | @underAbs k a b@ applies @k@ to @a@ and the content of
---   abstraction @b@ and puts the abstraction back.
---   @a@ is raised if abstraction was proper such that
---   at point of application of @k@ and the content of @b@
---   are at the same context.
---   Precondition: @a@ and @b@ are at the same context at call time.
-underAbs :: Subst a => (a -> b -> b) -> a -> Abs b -> Abs b
-underAbs cont a = \case
-  Abs   x t -> Abs   x $ cont (raise 1 a) t
-  NoAbs x t -> NoAbs x $ cont a t
-
--- | @underLambdas n k a b@ drops @n@ initial 'Lam's from @b@,
---   performs operation @k@ on @a@ and the body of @b@,
---   and puts the 'Lam's back.  @a@ is raised correctly
---   according to the number of abstractions.
-underLambdas :: TermSubst a => Int -> (a -> Term -> Term) -> a -> Term -> Term
-underLambdas n cont = loop n where
-  loop 0 a = cont a
-  loop n a = \case
-    Lam h b -> Lam h $ underAbs (loop $ n-1) a b
-    _       -> __IMPOSSIBLE__