[ clean ] remove underLambdas and underAbs

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
 --

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__