diff --git a/src/Juvix/Compiler/Builtins/Effect.hs b/src/Juvix/Compiler/Builtins/Effect.hs
index 72f1a80c8f..221623e0ba 100644
--- a/src/Juvix/Compiler/Builtins/Effect.hs
+++ b/src/Juvix/Compiler/Builtins/Effect.hs
@@ -95,8 +95,9 @@ registerFun fi = do
       a =% b = (a ==% b) freeVars
       clauses :: [(Expression, Expression)]
       clauses =
-        [ (clauseLhsAsExpression c, c ^. clauseBody)
-          | c <- toList (fi ^. funInfoDef . funDefClauses)
+        [ (clauseLhsAsExpression op (toList pats), body)
+          | Just cls <- [unfoldLambdaClauses (fi ^. funInfoDef . funDefBody)],
+            (pats, body) <- toList cls
         ]
   case zipExactMay (fi ^. funInfoClauses) clauses of
     Nothing -> error "builtin has the wrong number of clauses"
diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs
index 60ab1c1fb1..5960852abc 100644
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/src/Juvix/Compiler/Concrete/Language.hs
@@ -358,6 +358,7 @@ deriving stock instance (Ord (FixitySyntaxDef 'Scoped))
 data FixityDef = FixityDef
   { _fixityDefSymbol :: S.Symbol,
     _fixityDefFixity :: Fixity,
+    -- | Used internally for printing parentheses.
     _fixityDefPrec :: Int
   }
   deriving stock (Show, Eq, Ord)
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index 7a7fc4e6b3..db3491de6b 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -312,7 +312,7 @@ preFunctionDef f = do
       Nothing ->
         map
           getPatternName
-          (head (f ^. Internal.funDefClauses) ^. Internal.clausePatterns)
+          (fst (Internal.unfoldLambda (f ^. Internal.funDefBody)))
 
     normalizeBuiltinName :: Maybe BuiltinFunction -> Text -> Text
     normalizeBuiltinName blt name = case blt of
@@ -378,7 +378,10 @@ mkFunBody ::
   Internal.FunctionDef ->
   Sem r Node
 mkFunBody ty f =
-  mkBody ty (f ^. Internal.funDefName . nameLoc) (fmap (\c -> (c ^. Internal.clausePatterns, c ^. Internal.clauseBody)) (f ^. Internal.funDefClauses))
+  mkBody
+    ty
+    (f ^. Internal.funDefName . nameLoc)
+    (pure (Internal.unfoldLambda (f ^. Internal.funDefBody)))
 
 mkBody ::
   forall r.
diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs
index 838ec2af0d..28cfe72cd7 100644
--- a/src/Juvix/Compiler/Internal/Extra.hs
+++ b/src/Juvix/Compiler/Internal/Extra.hs
@@ -81,7 +81,7 @@ genFieldProjection ::
   Int ->
   Sem r FunctionDef
 genFieldProjection _funDefName info fieldIx = do
-  clause <- genClause
+  body' <- genBody
   let (inductiveParams, constrArgs) = constructorArgTypes info
       implicity = constructorImplicity info
       saturatedTy = unnamedParameter' implicity (constructorReturnType info)
@@ -94,18 +94,22 @@ genFieldProjection _funDefName info fieldIx = do
         _funDefInstance = False,
         _funDefBuiltin = Nothing,
         _funDefPragmas = mempty,
-        _funDefClauses = pure clause,
+        _funDefBody = body',
         _funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy,
         ..
       }
   where
-    genClause :: Sem r FunctionClause
-    genClause = do
+    genBody :: Sem r Expression
+    genBody = do
       (pat, vars) <- genConstructorPattern (getLoc _funDefName) info
       let body = toExpression (vars !! fieldIx)
-      return
-        FunctionClause
-          { _clauseName = _funDefName,
-            _clausePatterns = [pat],
-            _clauseBody = body
+          cl =
+            LambdaClause
+              { _lambdaPatterns = pure pat,
+                _lambdaBody = body
+              }
+      return . ExpressionLambda $
+        Lambda
+          { _lambdaType = Nothing,
+            _lambdaClauses = pure cl
           }
diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs
index 32968cee7a..f4b9063227 100644
--- a/src/Juvix/Compiler/Internal/Extra/Base.hs
+++ b/src/Juvix/Compiler/Internal/Extra/Base.hs
@@ -158,24 +158,17 @@ subsHoles s = over leafExpressions helper
       ExpressionInstanceHole h -> fromMaybe e (s ^. at h)
       _ -> e
 
-instance HasExpressions FunctionClause where
-  leafExpressions f c = do
-    _clauseBody <- leafExpressions f (c ^. clauseBody)
-    _clausePatterns <- traverse (leafExpressions f) (c ^. clausePatterns)
-    pure FunctionClause {_clauseName = c ^. clauseName, ..}
-
 instance HasExpressions Example where
   leafExpressions f = traverseOf exampleExpression (leafExpressions f)
 
 instance HasExpressions FunctionDef where
-  -- leafExpressions f (FunctionDef name ty clauses bi) = do
   leafExpressions f FunctionDef {..} = do
-    clauses' <- traverse (leafExpressions f) _funDefClauses
+    body' <- leafExpressions f _funDefBody
     ty' <- leafExpressions f _funDefType
     examples' <- traverse (leafExpressions f) _funDefExamples
     pure
       FunctionDef
-        { _funDefClauses = clauses',
+        { _funDefBody = body',
           _funDefType = ty',
           _funDefExamples = examples',
           _funDefTerminating,
@@ -316,6 +309,21 @@ viewConstructorType = first (map (^. paramType)) . unfoldFunType
 constructorArgs :: Expression -> [Expression]
 constructorArgs = fst . viewConstructorType
 
+unfoldLambdaClauses :: Expression -> Maybe (NonEmpty (NonEmpty PatternArg, Expression))
+unfoldLambdaClauses t = do
+  ExpressionLambda Lambda {..} <- return t
+  let mkClause :: LambdaClause -> (NonEmpty PatternArg, Expression)
+      mkClause LambdaClause {..} = first (appendList _lambdaPatterns) (unfoldLambda _lambdaBody)
+  return (mkClause <$> _lambdaClauses)
+
+-- Unfolds *single* clause lambdas
+unfoldLambda :: Expression -> ([PatternArg], Expression)
+unfoldLambda t = case t of
+  ExpressionLambda Lambda {..}
+    | LambdaClause {..} :| [] <- _lambdaClauses ->
+        first (toList _lambdaPatterns <>) (unfoldLambda _lambdaBody)
+  _ -> ([], t)
+
 -- | a -> (b -> c)  ==> ([a, b], c)
 unfoldFunType :: Expression -> ([FunctionParameter], Expression)
 unfoldFunType t = case t of
@@ -513,9 +521,9 @@ leftEq a b free =
     . evalState (mempty @(HashMap Name Name))
     $ matchExpressions (toExpression a) (toExpression b)
 
-clauseLhsAsExpression :: FunctionClause -> Expression
-clauseLhsAsExpression cl =
-  foldApplication (toExpression (cl ^. clauseName)) (map toApplicationArg (cl ^. clausePatterns))
+clauseLhsAsExpression :: Name -> [PatternArg] -> Expression
+clauseLhsAsExpression clName pats =
+  foldApplication (toExpression clName) (map toApplicationArg pats)
 
 infix 4 ==%
 
diff --git a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
index 07355c9a8e..8f0cbff80b 100644
--- a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
+++ b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
@@ -195,7 +195,7 @@ goFunctionDefHelper f = do
   when (f ^. funDefInstance) $
     goInstance f
   goExpression (Just (f ^. funDefName)) (f ^. funDefType)
-  mapM_ (goFunctionClause (f ^. funDefName)) (f ^. funDefClauses)
+  goExpression (Just (f ^. funDefName)) (f ^. funDefBody)
 
 -- constructors of an inductive type depend on the inductive type, not the other
 -- way round; an inductive type depends on the types of its constructors
@@ -204,11 +204,6 @@ goConstructorDef indName c = do
   addEdge (c ^. inductiveConstructorName) indName
   goExpression (Just indName) (c ^. inductiveConstructorType)
 
-goFunctionClause :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> FunctionClause -> Sem r ()
-goFunctionClause p c = do
-  mapM_ (goPattern (Just p)) (c ^. clausePatterns)
-  goExpression (Just p) (c ^. clauseBody)
-
 goPattern :: forall r. (Member (State DependencyGraph) r) => Maybe Name -> PatternArg -> Sem r ()
 goPattern n p = case p ^. patternArgPattern of
   PatternVariable {} -> return ()
diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs
index d78effc9b1..476e20c06a 100644
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/src/Juvix/Compiler/Internal/Language.hs
@@ -86,7 +86,7 @@ data FunctionDef = FunctionDef
   { _funDefName :: FunctionName,
     _funDefType :: Expression,
     _funDefExamples :: [Example],
-    _funDefClauses :: NonEmpty FunctionClause,
+    _funDefBody :: Expression,
     _funDefTerminating :: Bool,
     _funDefInstance :: Bool,
     _funDefBuiltin :: Maybe BuiltinFunction,
@@ -96,15 +96,6 @@ data FunctionDef = FunctionDef
 
 instance Hashable FunctionDef
 
-data FunctionClause = FunctionClause
-  { _clauseName :: FunctionName,
-    _clausePatterns :: [PatternArg],
-    _clauseBody :: Expression
-  }
-  deriving stock (Eq, Generic, Data)
-
-instance Hashable FunctionClause
-
 data Iden
   = IdenFunction Name
   | IdenConstructor Name
@@ -214,7 +205,7 @@ data Lambda = Lambda
   deriving stock (Eq, Generic, Data)
 
 data LambdaClause = LambdaClause
-  { _lambdaPatterns :: NonEmpty PatternArg, -- only explicit patterns are allowed
+  { _lambdaPatterns :: NonEmpty PatternArg,
     _lambdaBody :: Expression
   }
   deriving stock (Eq, Generic, Data)
@@ -327,7 +318,6 @@ makeLenses ''Example
 makeLenses ''PatternArg
 makeLenses ''Import
 makeLenses ''FunctionDef
-makeLenses ''FunctionClause
 makeLenses ''InductiveDef
 makeLenses ''AxiomDef
 makeLenses ''ModuleBody'
@@ -438,11 +428,8 @@ instance HasLoc LambdaClause where
 instance HasLoc Lambda where
   getLoc l = getLocSpan (l ^. lambdaClauses)
 
-instance HasLoc FunctionClause where
-  getLoc f = getLoc (f ^. clauseName) <> getLoc (f ^. clauseBody)
-
 instance HasLoc FunctionDef where
-  getLoc f = getLoc (f ^. funDefName) <> getLocSpan (f ^. funDefClauses)
+  getLoc f = getLoc (f ^. funDefName) <> getLoc (f ^. funDefBody)
 
 instance HasLoc MutualBlockLet where
   getLoc (MutualBlockLet defs) = getLocSpan defs
diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs
index fbbaf2dbbf..9910be7da5 100644
--- a/src/Juvix/Compiler/Internal/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs
@@ -238,26 +238,18 @@ instance PrettyCode FunctionDef where
     builtin' <- fmap (kwBuiltin <+>) <$> mapM ppCode (f ^. funDefBuiltin)
     funDefName' <- ppCode (f ^. funDefName)
     funDefType' <- ppCode (f ^. funDefType)
-    clauses' <- mapM ppCode (f ^. funDefClauses)
+    body' <- ppCode (f ^. funDefBody)
     return $
       builtin'
         <?+> funDefName'
           <+> kwColon
           <+> funDefType'
-            <> hardline
-            <> vsep (toList clauses')
+            <> oneLineOrNext (kwAssign <+> body')
 
 instance PrettyCode PreLetStatement where
   ppCode = \case
     PreLetFunctionDef f -> ppCode f
 
-instance PrettyCode FunctionClause where
-  ppCode c = do
-    funName <- ppCode (c ^. clauseName)
-    clausePatterns' <- hsepMaybe <$> mapM ppCodeAtom (c ^. clausePatterns)
-    clauseBody' <- ppCode (c ^. clauseBody)
-    return $ nest 2 (funName <+?> clausePatterns' <+> kwAssign <+> clauseBody')
-
 instance PrettyCode Import where
   ppCode i = do
     name' <- ppCode (i ^. importModule . moduleIxModule . moduleName)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 368758d54f..aa01ef04b3 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -435,28 +435,34 @@ goTopFunctionDef FunctionDef {..} = do
   _funDefType <- goDefType
   _funDefExamples <- goExamples _signDoc
   _funDefPragmas <- goPragmas _signPragmas
-  _funDefClauses <- goBody
+  _funDefBody <- goBody
   let fun = Internal.FunctionDef {..}
   whenJust _signBuiltin (registerBuiltinFunction fun . (^. withLocParam))
   return fun
   where
-    goBody :: Sem r (NonEmpty Internal.FunctionClause)
+    goBody :: Sem r Internal.Expression
     goBody = do
       commonPatterns <- concatMapM (fmap toList . argToPattern) _signArgs
-      let _clauseName = goSymbol _signName
-          goClause :: FunctionClause 'Scoped -> Sem r Internal.FunctionClause
+      let goClause :: FunctionClause 'Scoped -> Sem r Internal.LambdaClause
           goClause FunctionClause {..} = do
-            let _clauseName = goSymbol _signName
-            _clauseBody <- goExpression _clausenBody
-            extraPatterns <- toList <$> (mapM goPatternArg _clausenPatterns)
-            let _clausePatterns = commonPatterns <> extraPatterns
-            return Internal.FunctionClause {..}
+            _lambdaBody <- goExpression _clausenBody
+            extraPatterns <- mapM goPatternArg _clausenPatterns
+            let _lambdaPatterns = prependList commonPatterns extraPatterns
+            return Internal.LambdaClause {..}
       case _signBody of
         SigBodyExpression body -> do
-          _clauseBody <- goExpression body
-          let _clausePatterns = commonPatterns
-          return (pure Internal.FunctionClause {..})
-        SigBodyClauses cls -> mapM goClause cls
+          body' <- goExpression body
+          return $ case nonEmpty commonPatterns of
+            Nothing -> body'
+            Just _lambdaPatterns -> do
+              let _lambdaBody = body'
+                  _lambdaType :: Maybe Internal.Expression = Nothing
+                  _lambdaClauses = pure Internal.LambdaClause {..}
+              Internal.ExpressionLambda Internal.Lambda {..}
+        SigBodyClauses cls -> do
+          _lambdaClauses <- mapM goClause cls
+          let _lambdaType :: Maybe Internal.Expression = Nothing
+          return (Internal.ExpressionLambda Internal.Lambda {..})
 
     goDefType :: Sem r Internal.Expression
     goDefType = do
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
index 5ca7f1e09d..4ddbc06521 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
@@ -5,7 +5,6 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.C
 where
 
 import Juvix.Compiler.Internal.Extra
-import Juvix.Compiler.Internal.Pretty
 import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.LocalVars
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types
@@ -132,11 +131,11 @@ checkFunctionDef ::
 checkFunctionDef FunctionDef {..} = do
   let arity = typeArity _funDefType
   _funDefType' <- withEmptyLocalVars (checkType _funDefType)
-  _funDefClauses' <- mapM (checkFunctionClause arity) _funDefClauses
+  _funDefBody' <- checkFunctionBody arity _funDefBody
   _funDefExamples' <- withEmptyLocalVars (mapM checkExample _funDefExamples)
   return
     FunctionDef
-      { _funDefClauses = _funDefClauses',
+      { _funDefBody = _funDefBody',
         _funDefExamples = _funDefExamples',
         _funDefType = _funDefType',
         _funDefName,
@@ -146,24 +145,32 @@ checkFunctionDef FunctionDef {..} = do
         _funDefPragmas
       }
 
-checkFunctionClause ::
+checkFunctionBody ::
   (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
   Arity ->
-  FunctionClause ->
-  Sem r FunctionClause
-checkFunctionClause ari cl = do
-  hint <- guessArity (cl ^. clauseBody)
-  (patterns', locals, bodyAri) <- checkLhs loc hint ari (cl ^. clausePatterns)
-  body' <- runReader locals (checkExpression bodyAri (cl ^. clauseBody))
-  return
-    FunctionClause
-      { _clauseName = cl ^. clauseName,
-        _clausePatterns = patterns',
-        _clauseBody = body'
-      }
-  where
-    name = cl ^. clauseName
-    loc = getLoc name
+  Expression ->
+  Sem r Expression
+checkFunctionBody ari body = do
+  case body of
+    ExpressionLambda {} ->
+      withEmptyLocalVars (checkExpression ari body)
+    _ -> do
+      hint <- guessArity body
+      (patterns', locals, bodyAri) <- checkLhs (getLoc body) hint ari []
+      body' <- runReader locals (checkExpression bodyAri body)
+      return $ case nonEmpty patterns' of
+        Nothing -> body'
+        Just lambdaPatterns' ->
+          ExpressionLambda
+            Lambda
+              { _lambdaType = Nothing,
+                _lambdaClauses =
+                  pure
+                    LambdaClause
+                      { _lambdaPatterns = lambdaPatterns',
+                        _lambdaBody = body'
+                      }
+              }
 
 simplelambda :: a
 simplelambda = error "simple lambda expressions are not supported by the arity checker"
@@ -468,39 +475,23 @@ checkLambda ::
   Sem r Lambda
 checkLambda ari l = do
   let _lambdaType = l ^. lambdaType
-  _lambdaClauses <- mapM goClause (l ^. lambdaClauses)
+  _lambdaClauses <- mapM checkLambdaClause (l ^. lambdaClauses)
   return Lambda {..}
   where
-    goClause :: LambdaClause -> Sem r LambdaClause
-    goClause (LambdaClause ps b) = do
-      locals <- ask
-      let uari@UnfoldedArity {..} = unfoldArity' ari
-      (locals', (ps', rest)) <- runState locals (helper _ufoldArityRest (toList ps) _ufoldArityParams)
-      let ariBody = foldArity (set ufoldArityParams rest uari)
-      b' <- local (const locals') (checkExpression ariBody b)
-      return (LambdaClause (fromJust (nonEmpty ps')) b')
+    checkLambdaClause ::
+      LambdaClause ->
+      Sem r LambdaClause
+    checkLambdaClause cl = do
+      hint <- guessArity (cl ^. lambdaBody)
+      (patterns', locals, bodyAri) <- checkLhs loc hint ari (toList (cl ^. lambdaPatterns))
+      body' <- runReader locals (checkExpression bodyAri (cl ^. lambdaBody))
+      return
+        LambdaClause
+          { _lambdaPatterns = nonEmpty' patterns',
+            _lambdaBody = body'
+          }
       where
-        -- returns the adjusted patterns and the not consumed arity
-        helper :: ArityRest -> [PatternArg] -> [ArityParameter] -> Sem (State LocalVars ': r) ([PatternArg], [ArityParameter])
-        helper rest = go
-          where
-            go :: [PatternArg] -> [ArityParameter] -> Sem (State LocalVars ': r) ([PatternArg], [ArityParameter])
-            go pats as =
-              case (pats, as) of
-                ([], _) -> return ([], as)
-                (p : ps', ParamExplicit paramAri : as') -> do
-                  p' <- checkPattern paramAri p
-                  first (p' :) <$> go ps' as'
-                (_ : _, ParamImplicit {} : _) ->
-                  -- The lambda is expected to have an implicit argument but it cannot have one.
-                  -- TODO. think what to do in this case
-                  return (pats, as)
-                (_ : _, ParamImplicitInstance {} : _) ->
-                  -- TODO. think what to do in this case
-                  return (pats, as)
-                (_ : _, []) -> case rest of
-                  ArityRestUnit -> error ("too many patterns in lambda: " <> ppTrace l <> "\n" <> prettyText ari)
-                  ArityRestUnknown -> return (pats, [])
+        loc = getLoc cl
 
 idenArity :: (Members '[Reader LocalVars, Reader InfoTable] r) => Iden -> Sem r Arity
 idenArity = \case
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs
index 1dd2b4a692..c3362c132f 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs
@@ -104,10 +104,7 @@ checkStrictlyPositiveOccurrences ty ctorName name recLimit ref =
         helperFunctionDef :: FunctionDef -> Sem r ()
         helperFunctionDef d = do
           helper inside (d ^. funDefType)
-          mapM_ helperFunctionClause (d ^. funDefClauses)
-
-        helperFunctionClause :: FunctionClause -> Sem r ()
-        helperFunctionClause c = helper inside (c ^. clauseBody)
+          helper inside (d ^. funDefBody)
 
         helperSimpleLambda :: SimpleLambda -> Sem r ()
         helperSimpleLambda (SimpleLambda _ lamVarTy lamBody) = do
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs
index 55409af861..b32e4e3512 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs
@@ -147,7 +147,7 @@ scanFunctionDef f@FunctionDef {..} = do
   registerFunctionDef f
   runReader (Just _funDefName) $ do
     scanTypeSignature _funDefType
-    mapM_ scanFunctionClause _funDefClauses
+    scanFunctionBody _funDefBody
 
 scanTypeSignature ::
   (Members '[State CallMap, Reader (Maybe FunctionRef)] r) =>
@@ -155,12 +155,12 @@ scanTypeSignature ::
   Sem r ()
 scanTypeSignature = runReader emptySizeInfo . scanExpression
 
-scanFunctionClause ::
+scanFunctionBody ::
   forall r.
   (Members '[State CallMap, Reader (Maybe FunctionRef)] r) =>
-  FunctionClause ->
+  Expression ->
   Sem r ()
-scanFunctionClause FunctionClause {..} = go (reverse _clausePatterns) _clauseBody
+scanFunctionBody topbody = go [] topbody
   where
     go :: [PatternArg] -> Expression -> Sem r ()
     go revArgs body = case body of
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
index 4c24b8d9cb..36295d9264 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
@@ -184,10 +184,10 @@ checkFunctionDef FunctionDef {..} = do
   funDef <- do
     _funDefType' <- checkDefType _funDefType
     registerIdenType _funDefName _funDefType'
-    _funDefClauses' <- mapM (checkFunctionClause _funDefType') _funDefClauses
+    _funDefBody' <- checkExpression _funDefType' _funDefBody
     return
       FunctionDef
-        { _funDefClauses = _funDefClauses',
+        { _funDefBody = _funDefBody',
           _funDefType = _funDefType',
           ..
         }
@@ -369,21 +369,6 @@ lookupVar v = HashMap.lookupDefault err v <$> asks (^. localTypes)
   where
     err = error $ "internal error: could not find var " <> ppTrace v
 
-checkFunctionClause ::
-  forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Inference, Builtins, State TypesTable, Output Example, Reader LocalVars, Termination, Output TypedHole] r) =>
-  Expression ->
-  FunctionClause ->
-  Sem r FunctionClause
-checkFunctionClause clauseType FunctionClause {..} = do
-  (patterns', body') <- checkClause clauseType _clausePatterns _clauseBody
-  return
-    FunctionClause
-      { _clauseBody = body',
-        _clausePatterns = patterns',
-        ..
-      }
-
 -- | helper function for function clauses and lambda functions
 checkClause ::
   forall r.
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
index 9eff10a710..ea22030fc1 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
@@ -472,22 +472,24 @@ functionDefEval f = do
       Sem r Expression
     goTop params returnsType = do
       checkTerminating
-      case f ^. funDefClauses of
-        c :| [] -> goClause c
-        _ -> fail
+      goBody (f ^. funDefBody)
       where
         checkTerminating :: Sem r ()
         checkTerminating = unlessM (functionIsTerminating (f ^. funDefName)) fail
 
-        goClause :: FunctionClause -> Sem r Expression
-        goClause c = do
-          let pats = c ^. clausePatterns
+        goBody :: Expression -> Sem r Expression
+        goBody body = do
+          checkOneClause
           patsTys <- splitExplicitParams
           go (zipExact pats patsTys)
           where
+            (pats, body') = unfoldLambda body
+            checkOneClause = case body of
+              ExpressionLambda Lambda {_lambdaClauses = _ :| _ : _} -> fail
+              _ -> return ()
             splitExplicitParams :: Sem r [Expression]
             splitExplicitParams = do
-              let n = length (c ^. clausePatterns)
+              let n = length pats
               unless returnsType fail
               nfirst <- failMaybe (takeExactMay n params)
               mapM simpleExplicitParam nfirst
@@ -501,7 +503,7 @@ functionDefEval f = do
               _ -> const fail
             go :: [(PatternArg, Expression)] -> Sem r Expression
             go = \case
-              [] -> return (c ^. clauseBody)
+              [] -> return body'
               (p, ty) : ps
                 | Implicit <- p ^. patternArgIsImplicit -> fail
                 | otherwise -> go ps >>= goPattern (p ^. patternArgPattern, ty)
diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index fe385df255..134ac33c3c 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -117,6 +117,7 @@ import Data.List.Extra qualified as List
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.List.NonEmpty.Extra
   ( NonEmpty (..),
+    appendList,
     head,
     last,
     maximum1,
@@ -124,6 +125,7 @@ import Data.List.NonEmpty.Extra
     minimum1,
     minimumOn1,
     nonEmpty,
+    prependList,
     some1,
     (|:),
   )