diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs
index 7ef1677d59..780abf4753 100644
--- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs
+++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs
@@ -58,10 +58,13 @@ instance (SingI s) => HasNameSignature s (AxiomDef s) where
   addArgs :: (Members '[NameSignatureBuilder s] r) => AxiomDef s -> Sem r ()
   addArgs a = addExpressionType (a ^. axiomType)
 
-instance (SingI s) => HasNameSignature s (FunctionDef s) where
+instance (SingI s) => HasNameSignature s (FunctionLhs s) where
   addArgs a = do
-    mapM_ addSigArg (a ^. signArgs)
-    whenJust (a ^. signRetType) addExpressionType
+    mapM_ addSigArg (a ^. funLhsArgs)
+    whenJust (a ^. funLhsRetType) addExpressionType
+
+instance (SingI s) => HasNameSignature s (FunctionDef s) where
+  addArgs = addArgs . functionDefLhs
 
 instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) where
   addArgs ::
diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs
index 64335c2233..e47e44c402 100644
--- a/src/Juvix/Compiler/Concrete/Extra.hs
+++ b/src/Juvix/Compiler/Concrete/Extra.hs
@@ -9,6 +9,7 @@ module Juvix.Compiler.Concrete.Extra
     getPatternAtomIden,
     isBodyExpression,
     isFunctionLike,
+    isLhsFunctionLike,
     symbolParsed,
   )
 where
@@ -46,6 +47,8 @@ groupStatements = \case
     -- blank line
     g :: Statement s -> Statement s -> Bool
     g a b = case (a, b) of
+      (StatementDeriving _, StatementDeriving _) -> True
+      (StatementDeriving _, _) -> False
       (StatementSyntax _, StatementSyntax _) -> True
       (StatementSyntax (SyntaxFixity _), _) -> False
       (StatementSyntax (SyntaxOperator o), s) -> definesSymbol (o ^. opSymbol) s
@@ -108,6 +111,9 @@ isBodyExpression = \case
   SigBodyExpression {} -> True
   SigBodyClauses {} -> False
 
+isLhsFunctionLike :: FunctionLhs 'Parsed -> Bool
+isLhsFunctionLike FunctionLhs {..} = not (null _funLhsArgs)
+
 isFunctionLike :: FunctionDef 'Parsed -> Bool
-isFunctionLike = \case
-  FunctionDef {..} -> not (null _signArgs) || maybe False (not . isBodyExpression) _signBody
+isFunctionLike d@FunctionDef {..} =
+   isLhsFunctionLike (functionDefLhs d) || (not . isBodyExpression) _signBody
diff --git a/src/Juvix/Compiler/Concrete/Gen.hs b/src/Juvix/Compiler/Concrete/Gen.hs
index a16df951e3..2b310482ac 100644
--- a/src/Juvix/Compiler/Concrete/Gen.hs
+++ b/src/Juvix/Compiler/Concrete/Gen.hs
@@ -24,11 +24,11 @@ simplestFunctionDefParsed funNameTxt funBody = do
   funName <- symbol funNameTxt
   return (simplestFunctionDef funName (mkExpressionAtoms funBody))
 
-simplestFunctionDef :: forall s. (SingI s) => FunctionName s -> ExpressionType s -> FunctionDef s
+simplestFunctionDef :: FunctionName s -> ExpressionType s -> FunctionDef s
 simplestFunctionDef funName funBody =
   FunctionDef
     { _signName = funName,
-      _signBody = body,
+      _signBody = SigBodyExpression funBody,
       _signColonKw = Irrelevant Nothing,
       _signArgs = [],
       _signRetType = Nothing,
@@ -36,15 +36,9 @@ simplestFunctionDef funName funBody =
       _signPragmas = Nothing,
       _signBuiltin = Nothing,
       _signTerminating = Nothing,
-      _signDeriving = Nothing,
       _signInstance = Nothing,
       _signCoercion = Nothing
     }
-  where
-    body :: FunctionDefBodyType s
-    body = case sing :: SStage s of
-      SParsed -> Just (SigBodyExpression funBody)
-      SScoped -> SigBodyExpression funBody
 
 smallUniverseExpression :: forall s r. (SingI s) => (Members '[Reader Interval] r) => Sem r (ExpressionType s)
 smallUniverseExpression = do
diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs
index 01af93aac0..6b332ab8b8 100644
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/src/Juvix/Compiler/Concrete/Language.hs
@@ -31,6 +31,7 @@ statementLabel = \case
   StatementOpenModule {} -> Nothing
   StatementProjectionDef {} -> Nothing
   StatementFunctionDef f -> Just (f ^. signName . symbolTypeLabel)
+  StatementDeriving f -> Just (f ^. derivingFunLhs . funLhsName . symbolTypeLabel)
   StatementImport i -> Just (i ^. importModulePath . to modulePathTypeLabel)
   StatementInductive i -> Just (i ^. inductiveName . symbolTypeLabel)
   StatementModule i -> Just (i ^. modulePath . to modulePathTypeLabel)
diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
index 3c8782e4da..c009fd0b1b 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -55,11 +55,6 @@ type family FieldArgIxType s = res | res -> s where
   FieldArgIxType 'Parsed = ()
   FieldArgIxType 'Scoped = Int
 
-type FunctionDefBodyType :: Stage -> GHCType
-type family FunctionDefBodyType s = res | res -> s where
-  FunctionDefBodyType 'Parsed = Maybe (FunctionDefBody 'Parsed)
-  FunctionDefBodyType 'Scoped = FunctionDefBody 'Scoped
-
 type SideIfBranchConditionType :: Stage -> IfBranchKind -> GHCType
 type family SideIfBranchConditionType s k = res where
   SideIfBranchConditionType s 'BranchIfBool = ExpressionType s
@@ -276,6 +271,7 @@ data NonDefinitionsSection (s :: Stage) = NonDefinitionsSection
 data Definition (s :: Stage)
   = DefinitionSyntax (SyntaxDef s)
   | DefinitionFunctionDef (FunctionDef s)
+  | DefinitionDeriving (Deriving s)
   | DefinitionInductive (InductiveDef s)
   | DefinitionAxiom (AxiomDef s)
   | DefinitionProjectionDef (ProjectionDef s)
@@ -292,6 +288,7 @@ newtype Statements (s :: Stage) = Statements
 data Statement (s :: Stage)
   = StatementSyntax (SyntaxDef s)
   | StatementFunctionDef (FunctionDef s)
+  | StatementDeriving (Deriving s)
   | StatementImport (Import s)
   | StatementInductive (InductiveDef s)
   | StatementModule (Module s 'ModuleLocal)
@@ -650,6 +647,32 @@ deriving stock instance Ord (FunctionDefBody 'Parsed)
 
 deriving stock instance Ord (FunctionDefBody 'Scoped)
 
+data Deriving (s :: Stage) = Deriving
+  { _derivingKw :: KeywordRef,
+    _derivingFunLhs :: FunctionLhs s
+  }
+  deriving stock (Generic)
+
+instance Serialize (Deriving 'Scoped)
+
+instance NFData (Deriving 'Scoped)
+
+instance Serialize (Deriving 'Parsed)
+
+instance NFData (Deriving 'Parsed)
+
+deriving stock instance Show (Deriving 'Parsed)
+
+deriving stock instance Show (Deriving 'Scoped)
+
+deriving stock instance Eq (Deriving 'Parsed)
+
+deriving stock instance Eq (Deriving 'Scoped)
+
+deriving stock instance Ord (Deriving 'Parsed)
+
+deriving stock instance Ord (Deriving 'Scoped)
+
 data FunctionDef (s :: Stage) = FunctionDef
   { _signName :: FunctionName s,
     _signArgs :: [SigArg s],
@@ -658,10 +681,8 @@ data FunctionDef (s :: Stage) = FunctionDef
     _signDoc :: Maybe (Judoc s),
     _signPragmas :: Maybe ParsedPragmas,
     _signBuiltin :: Maybe (WithLoc BuiltinFunction),
-    -- | Only deriving instances can omit the body
-    _signBody :: FunctionDefBodyType s,
+    _signBody :: FunctionDefBody s,
     _signTerminating :: Maybe KeywordRef,
-    _signDeriving :: Maybe KeywordRef,
     _signInstance :: Maybe KeywordRef,
     _signCoercion :: Maybe KeywordRef
   }
@@ -2814,13 +2835,33 @@ data FunctionLhs (s :: Stage) = FunctionLhs
   { _funLhsBuiltin :: Maybe (WithLoc BuiltinFunction),
     _funLhsTerminating :: Maybe KeywordRef,
     _funLhsInstance :: Maybe KeywordRef,
-    _funLhsDeriving :: Maybe KeywordRef,
     _funLhsCoercion :: Maybe KeywordRef,
     _funLhsName :: FunctionName s,
     _funLhsArgs :: [SigArg s],
     _funLhsColonKw :: Irrelevant (Maybe KeywordRef),
     _funLhsRetType :: Maybe (ExpressionType s)
   }
+  deriving stock (Generic)
+
+instance Serialize (FunctionLhs 'Scoped)
+
+instance NFData (FunctionLhs 'Scoped)
+
+instance Serialize (FunctionLhs 'Parsed)
+
+instance NFData (FunctionLhs 'Parsed)
+
+deriving stock instance Show (FunctionLhs 'Parsed)
+
+deriving stock instance Show (FunctionLhs 'Scoped)
+
+deriving stock instance Eq (FunctionLhs 'Parsed)
+
+deriving stock instance Eq (FunctionLhs 'Scoped)
+
+deriving stock instance Ord (FunctionLhs 'Parsed)
+
+deriving stock instance Ord (FunctionLhs 'Scoped)
 
 makeLenses ''SideIfs
 makeLenses ''FunctionLhs
@@ -2908,6 +2949,8 @@ makeLenses ''NameBlock
 makeLenses ''NameItem
 makeLenses ''RecordInfo
 makeLenses ''MarkdownInfo
+makeLenses ''Deriving
+
 makePrisms ''NamedArgumentNew
 
 functionDefLhs :: FunctionDef s -> FunctionLhs s
@@ -2919,7 +2962,6 @@ functionDefLhs FunctionDef {..} =
       _funLhsCoercion = _signCoercion,
       _funLhsName = _signName,
       _funLhsArgs = _signArgs,
-      _funLhsDeriving = _signDeriving,
       _funLhsColonKw = _signColonKw,
       _funLhsRetType = _signRetType
     }
@@ -3083,10 +3125,16 @@ instance HasLoc (OpenModule s short) where
 instance HasLoc (ProjectionDef s) where
   getLoc = getLoc . (^. projectionConstructor)
 
+instance (SingI s) => HasLoc (Deriving s) where
+  getLoc Deriving {..} =
+    getLoc _derivingKw
+      <> getLoc _derivingFunLhs
+
 instance HasLoc (Statement 'Scoped) where
   getLoc :: Statement 'Scoped -> Interval
   getLoc = \case
     StatementSyntax t -> getLoc t
+    StatementDeriving t -> getLoc t
     StatementFunctionDef t -> getLoc t
     StatementImport t -> getLoc t
     StatementInductive t -> getLoc t
@@ -3313,23 +3361,22 @@ instance (SingI s) => HasLoc (FunctionDefBody s) where
     SigBodyExpression e -> getLocExpressionType e
     SigBodyClauses cl -> getLocSpan cl
 
+instance (SingI s) => HasLoc (FunctionLhs s) where
+  getLoc FunctionLhs {..} =
+    (getLoc <$> _funLhsBuiltin)
+      ?<> (getLoc <$> _funLhsTerminating)
+      ?<> ( getLocSymbolType _funLhsName
+              <>? (getLocExpressionType <$> _funLhsRetType)
+          )
+
 instance (SingI s) => HasLoc (FunctionDef s) where
   getLoc FunctionDef {..} =
     (getLoc <$> _signDoc)
       ?<> (getLoc <$> _signPragmas)
       ?<> (getLoc <$> _signBuiltin)
       ?<> (getLoc <$> _signTerminating)
-      ?<> ( getLocSymbolType _signName
-              <>? (getLocFunctionDefBodyType _signBody)
-          )
-
-getFunctionDefBodyType :: forall s. (SingI s) => FunctionDefBodyType s -> Maybe (FunctionDefBody s)
-getFunctionDefBodyType m = case sing :: SStage s of
-  SParsed -> m
-  SScoped -> Just m
-
-getLocFunctionDefBodyType :: forall s. (SingI s) => FunctionDefBodyType s -> Maybe Interval
-getLocFunctionDefBodyType = fmap getLoc . getFunctionDefBodyType
+      ?<> getLocSymbolType _signName
+      <> (getLoc _signBody)
 
 instance HasLoc (Example s) where
   getLoc e = e ^. exampleLoc
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 98229951e4..b2b7ea0d0c 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -1143,13 +1143,16 @@ instance (SingI s) => PrettyPrint (SigArg s) where
         defaultVal = ppCode <$> _sigArgDefault
     ppCode l <> arg <+?> defaultVal <> ppCode r
 
+instance (SingI s) => PrettyPrint (Deriving s) where
+  ppCode Deriving {..} =
+    ppCode _derivingKw
+      <+> ppCode _derivingFunLhs
+
 instance (SingI s) => PrettyPrint (FunctionLhs s) where
   ppCode FunctionLhs {..} = do
     let termin' = (<> line) . ppCode <$> _funLhsTerminating
         coercion' = (<> if isJust instance' then space else line) . ppCode <$> _funLhsCoercion
-        instance' = case _funLhsDeriving of
-          Nothing -> (<> line) . ppCode <$> _funLhsInstance
-          Just derKw -> Just (ppCode derKw <+> ppCode (fromJust _funLhsInstance) <> line)
+        instance' = (<> line) . ppCode <$> _funLhsInstance
         builtin' = (<> line) . ppCode <$> _funLhsBuiltin
         margs' = fmap ppCode <$> nonEmpty _funLhsArgs
         mtype' = case _funLhsColonKw ^. unIrrelevant of
@@ -1173,10 +1176,9 @@ instance (SingI s) => PrettyPrint (FunctionDef s) where
     let doc' :: Maybe (Sem r ()) = ppCode <$> _signDoc
         pragmas' :: Maybe (Sem r ()) = ppCode <$> _signPragmas
         sig' = ppCode (functionDefLhs fun)
-        body' = case getFunctionDefBodyType _signBody of
-          Nothing -> return ()
-          Just (SigBodyExpression e) -> space <> ppCode Kw.kwAssign <> oneLineOrNext (ppTopExpressionType e)
-          Just (SigBodyClauses k) -> line <> indent (vsep (ppCode <$> k))
+        body' = case _signBody of
+          SigBodyExpression e -> space <> ppCode Kw.kwAssign <> oneLineOrNext (ppTopExpressionType e)
+          SigBodyClauses k -> line <> indent (vsep (ppCode <$> k))
     doc'
       ?<> pragmas'
       ?<> sig'
@@ -1535,6 +1537,7 @@ instance (SingI s) => PrettyPrint (Statement s) where
   ppCode = \case
     StatementSyntax s -> ppCode s
     StatementFunctionDef f -> ppCode f
+    StatementDeriving f -> ppCode f
     StatementImport i -> ppCode i
     StatementInductive i -> ppCode i
     StatementModule m -> ppCode m
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 86c2fc0933..c790b5b1b6 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -404,10 +404,10 @@ reserveConstructorSymbol d c b = do
 
 reserveFunctionSymbol ::
   (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
-  FunctionDef 'Parsed ->
+  FunctionLhs 'Parsed ->
   Sem r S.Symbol
 reserveFunctionSymbol f =
-  reserveSymbolSignatureOf SKNameFunction f (toBuiltinPrim <$> f ^. signBuiltin) (f ^. signName)
+  reserveSymbolSignatureOf SKNameFunction f (toBuiltinPrim <$> f ^. funLhsBuiltin) (f ^. funLhsName)
 
 reserveAxiomSymbol ::
   (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
@@ -419,37 +419,22 @@ reserveAxiomSymbol a =
     kindPretty :: NameKind
     kindPretty = maybe KNameAxiom getNameKind (a ^? axiomBuiltin . _Just . withLocParam)
 
+reserveDerivingSymbol ::
+  (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
+  Deriving 'Parsed ->
+  Sem r ()
+reserveDerivingSymbol f = do
+  let lhs = f ^. derivingFunLhs
+  when (P.isLhsFunctionLike lhs) $
+    void (reserveFunctionSymbol lhs)
+
 reserveFunctionLikeSymbol ::
   (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
   FunctionDef 'Parsed ->
   Sem r ()
 reserveFunctionLikeSymbol f =
   when (P.isFunctionLike f) $
-    void (reserveFunctionSymbol f)
-
-bindFunctionSymbol ::
-  (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) =>
-  Symbol ->
-  Sem r S.Symbol
-bindFunctionSymbol = getReservedDefinitionSymbol
-
-bindInductiveSymbol ::
-  (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) =>
-  Symbol ->
-  Sem r S.Symbol
-bindInductiveSymbol = getReservedDefinitionSymbol
-
-bindAxiomSymbol ::
-  (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) =>
-  Symbol ->
-  Sem r S.Symbol
-bindAxiomSymbol = getReservedDefinitionSymbol
-
-bindConstructorSymbol ::
-  (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) =>
-  Symbol ->
-  Sem r S.Symbol
-bindConstructorSymbol = getReservedDefinitionSymbol
+    void (reserveFunctionSymbol (functionDefLhs f))
 
 bindFixitySymbol ::
   (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) =>
@@ -1067,6 +1052,20 @@ resolveIteratorSyntaxDef s@IteratorSyntaxDef {..} = do
 (@$>) :: (Functor m) => (a -> m ()) -> a -> m a
 (@$>) f a = f a $> a
 
+withFunctionDefLhs ::
+  FunctionLhs 'Parsed ->
+  (FunctionLhs 'Scoped -> Sem r a)
+  Sem r a
+withFunctionDefLhs FunctionLhs {..} checkBody = do
+  body' <- withLocalScope $ do
+    args' <- mapM checkArg _funLhsArgs
+    ret' <- mapM checkParseExpressionAtoms _funLhsRetType
+    let lhs' = FunctionLhs {
+          _funLhsArgs = args',
+          _funLhsRetType = ret'
+                           }
+    checkBody lhs'
+
 checkFunctionDef ::
   forall r.
   (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, State ScoperSyntax, Reader BindingStrategy] r) =>
@@ -1081,8 +1080,8 @@ checkFunctionDef fdef@FunctionDef {..} = do
     return (a', t', b')
   sigName' <-
     if
-        | P.isFunctionLike fdef -> bindFunctionSymbol _signName
-        | otherwise -> reserveFunctionSymbol fdef
+        | P.isFunctionLike fdef -> getReservedDefinitionSymbol _signName
+        | otherwise -> reserveFunctionSymbol (functionDefLhs fdef)
   let def =
         FunctionDef
           { _signName = sigName',
@@ -1124,7 +1123,7 @@ checkFunctionDef fdef@FunctionDef {..} = do
             ..
           }
     checkBody :: Sem r (FunctionDefBody 'Scoped)
-    checkBody = case fromJust _signBody of -- FIXME
+    checkBody = case _signBody of
       SigBodyExpression e -> SigBodyExpression <$> checkParseExpressionAtoms e
       SigBodyClauses cls -> SigBodyClauses <$> mapM checkClause cls
 
@@ -1179,8 +1178,8 @@ checkInductiveDef ::
   Sem r (InductiveDef 'Scoped)
 checkInductiveDef InductiveDef {..} = do
   (inductiveName', constructorNames' :: NonEmpty S.Symbol) <- topBindings $ do
-    i <- bindInductiveSymbol _inductiveName
-    cs <- mapM (bindConstructorSymbol . (^. constructorName)) _inductiveConstructors
+    i <- getReservedDefinitionSymbol _inductiveName
+    cs <- mapM (getReservedDefinitionSymbol . (^. constructorName)) _inductiveConstructors
     return (i, cs)
   (inductiveParameters', inductiveType', inductiveTypeApplied', inductiveDoc', inductiveConstructors') <- withLocalScope $ do
     inductiveParameters' <- mapM checkInductiveParameters _inductiveParameters
@@ -1478,6 +1477,7 @@ checkModuleBody body = do
             toStatement :: Definition s -> Statement s
             toStatement = \case
               DefinitionSyntax d -> StatementSyntax d
+              DefinitionDeriving d -> StatementDeriving d
               DefinitionAxiom d -> StatementAxiom d
               DefinitionFunctionDef d -> StatementFunctionDef d
               DefinitionInductive d -> StatementInductive d
@@ -1613,6 +1613,7 @@ checkSections sec = topBindings helper
             reserveDefinition = \case
               DefinitionSyntax s -> resolveSyntaxDef s $> Nothing
               DefinitionFunctionDef d -> reserveFunctionLikeSymbol d >> return Nothing
+              DefinitionDeriving d -> reserveDerivingSymbol d >> return Nothing
               DefinitionAxiom d -> reserveAxiomSymbol d >> return Nothing
               DefinitionProjectionDef d -> reserveProjectionSymbol d >> return Nothing
               DefinitionInductive d -> Just <$> reserveInductive d
@@ -1668,6 +1669,7 @@ checkSections sec = topBindings helper
             goDefinition = \case
               DefinitionSyntax s -> DefinitionSyntax <$> checkSyntaxDef s
               DefinitionFunctionDef d -> DefinitionFunctionDef <$> checkFunctionDef d
+              DefinitionDeriving d -> DefinitionDeriving <$> checkDeriving d
               DefinitionAxiom d -> DefinitionAxiom <$> checkAxiomDef d
               DefinitionInductive d -> DefinitionInductive <$> checkInductiveDef d
               DefinitionProjectionDef d -> DefinitionProjectionDef <$> checkProjectionDef d
@@ -1808,6 +1810,7 @@ mkSections = \case
     fromStatement = \case
       StatementAxiom a -> Left (DefinitionAxiom a)
       StatementFunctionDef n -> Left (DefinitionFunctionDef n)
+      StatementDeriving n -> Left (DefinitionDeriving n)
       StatementInductive i -> Left (DefinitionInductive i)
       StatementSyntax s -> Left (DefinitionSyntax s)
       StatementProjectionDef s -> Left (DefinitionProjectionDef s)
@@ -2131,7 +2134,7 @@ checkAxiomDef ::
   Sem r (AxiomDef 'Scoped)
 checkAxiomDef AxiomDef {..} = do
   axiomType' <- withLocalScope (checkParseExpressionAtoms _axiomType)
-  axiomName' <- bindAxiomSymbol _axiomName
+  axiomName' <- getReservedDefinitionSymbol _axiomName
   axiomDoc' <- withLocalScope (mapM checkJudoc _axiomDoc)
   let a = AxiomDef {_axiomName = axiomName', _axiomType = axiomType', _axiomDoc = axiomDoc', ..}
   registerNameSignature (a ^. axiomName . S.nameId) a
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index e271de4ec1..db5d3be01e 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -1305,7 +1305,6 @@ functionDefinitionLhs opts _funLhsBuiltin = P.label "<function definition>" $ do
   return
     FunctionLhs
       { _funLhsInstance,
-        _funLhsDeriving,
         _funLhsBuiltin,
         _funLhsCoercion,
         _funLhsName,
@@ -1366,10 +1365,7 @@ functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
   off <- P.getOffset
   _signDoc <- getJudoc
   _signPragmas <- getPragmas
-  _signBody <-
-    if
-        | isJust _funLhsDeriving -> return Nothing
-        | otherwise -> Just <$> parseBody
+  _signBody <- parseBody
   unless
     ( isJust (_funLhsColonKw ^. unIrrelevant)
         || (maybe True P.isBodyExpression _signBody && null _funLhsArgs)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 3aaeaa7731..924ecbaf27 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -315,6 +315,7 @@ scanImports = mconcatMap go
       StatementAxiom {} -> []
       StatementSyntax {} -> []
       StatementFunctionDef {} -> []
+      StatementDeriving {} -> []
       StatementProjectionDef {} -> []
 
 goImport ::
@@ -340,6 +341,7 @@ goAxiomInductive = \case
   StatementModule f -> goLocalModule f
   StatementImport {} -> return []
   StatementFunctionDef {} -> return []
+  StatementDeriving {} -> return []
   StatementSyntax {} -> return []
   StatementOpenModule {} -> return []
   StatementProjectionDef {} -> return []
@@ -542,7 +544,7 @@ checkBuiltinFunction ::
   Sem r ()
 checkBuiltinFunction d f = localBuiltins $ case f of
   BuiltinAssert -> checkAssert d
-  BuiltinIsEq -> checkIsEq d
+  BuiltinIsEqual -> checkIsEq d
   BuiltinNatPlus -> checkNatPlus d
   BuiltinNatSub -> checkNatSub d
   BuiltinNatMul -> checkNatMul d
diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader.hs b/src/Juvix/Compiler/Pipeline/Package/Loader.hs
index ccaf0e717f..137790a531 100644
--- a/src/Juvix/Compiler/Pipeline/Package/Loader.hs
+++ b/src/Juvix/Compiler/Pipeline/Package/Loader.hs
@@ -83,14 +83,13 @@ toConcrete t p = run . runReader l $ do
       _signRetType <- Just <$> expressionAtoms' (packageTypeIdentifier :| [])
       _signName <- symbol Str.package
       _signColonKw <- Irrelevant . Just <$> kw kwColon
-      let _signBody = Just ((t ^. packageDescriptionTypeTransform) p)
+      let _signBody = (t ^. packageDescriptionTypeTransform) p
       return
         ( StatementFunctionDef
             FunctionDef
               { _signTerminating = Nothing,
                 _signPragmas = Nothing,
                 _signInstance = Nothing,
-                _signDeriving = Nothing,
                 _signDoc = Nothing,
                 _signCoercion = Nothing,
                 _signBuiltin = Nothing,