diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs
index b4c5832f30..f236306025 100644
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/src/Juvix/Compiler/Concrete/Language.hs
@@ -292,7 +292,9 @@ data ProjectionDef s = ProjectionDef
   { _projectionConstructor :: S.Symbol,
     _projectionField :: SymbolType s,
     _projectionFieldIx :: Int,
-    _projectionFieldBuiltin :: Maybe (WithLoc BuiltinFunction)
+    _projectionFieldBuiltin :: Maybe (WithLoc BuiltinFunction),
+    _projectionDoc :: Maybe (Judoc s),
+    _projectionPragmas :: Maybe ParsedPragmas
   }
 
 deriving stock instance Show (ProjectionDef 'Parsed)
@@ -713,7 +715,9 @@ data RecordField (s :: Stage) = RecordField
   { _fieldName :: SymbolType s,
     _fieldColon :: Irrelevant (KeywordRef),
     _fieldType :: ExpressionType s,
-    _fieldBuiltin :: Maybe (WithLoc BuiltinFunction)
+    _fieldBuiltin :: Maybe (WithLoc BuiltinFunction),
+    _fieldDoc :: Maybe (Judoc s),
+    _fieldPragmas :: Maybe ParsedPragmas
   }
   deriving stock (Generic)
 
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 2fd4c1587d..4299ff2c04 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -1230,8 +1230,12 @@ instance (SingI s) => PrettyPrint (RhsGadt s) where
 
 instance (SingI s) => PrettyPrint (RecordField s) where
   ppCode RecordField {..} = do
-    let builtin' = (<> line) . ppCode <$> _fieldBuiltin
-    builtin'
+    let doc' = ppCode <$> _fieldDoc
+        pragmas' = ppCode <$> _fieldPragmas
+        builtin' = (<> line) . ppCode <$> _fieldBuiltin
+    doc'
+      ?<> pragmas'
+      ?<> builtin'
       ?<> ppSymbolType _fieldName
       <+> ppCode _fieldColon
       <+> ppExpressionType _fieldType
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index bbf3360f42..10ec1a39cf 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -158,17 +158,20 @@ freshVariable = freshSymbol KNameLocal KNameLocal
 
 checkProjectionDef ::
   forall r.
-  (Members '[Error ScoperError, InfoTableBuilder, Reader InfoTable, Reader BindingStrategy, State Scope, State ScoperState, NameIdGen, State ScoperSyntax] r) =>
+  (Members '[Error ScoperError, InfoTableBuilder, Reader Package, Reader ScopeParameters, Reader InfoTable, Reader BindingStrategy, State Scope, State ScoperState, NameIdGen, State ScoperSyntax] r) =>
   ProjectionDef 'Parsed ->
   Sem r (ProjectionDef 'Scoped)
 checkProjectionDef p = do
   _projectionField <- getReservedDefinitionSymbol (p ^. projectionField)
+  _projectionDoc <- maybe (return Nothing) (checkJudoc >=> return . Just) (p ^. projectionDoc)
   return
     ProjectionDef
       { _projectionFieldIx = p ^. projectionFieldIx,
         _projectionConstructor = p ^. projectionConstructor,
         _projectionFieldBuiltin = p ^. projectionFieldBuiltin,
-        _projectionField
+        _projectionPragmas = p ^. projectionPragmas,
+        _projectionField,
+        _projectionDoc
       }
 
 freshSymbol ::
@@ -1210,6 +1213,7 @@ checkInductiveDef InductiveDef {..} = do
 
             checkField :: RecordField 'Parsed -> Sem r (RecordField 'Scoped)
             checkField RecordField {..} = do
+              doc' <- maybe (return Nothing) (checkJudoc >=> return . Just) _fieldDoc
               type' <- checkParseExpressionAtoms _fieldType
               -- Since we don't allow dependent types in constructor types, each
               -- field is checked with a local scope
@@ -1219,6 +1223,7 @@ checkInductiveDef InductiveDef {..} = do
                   RecordField
                     { _fieldType = type',
                       _fieldName = name',
+                      _fieldDoc = doc',
                       ..
                     }
 
@@ -1629,7 +1634,9 @@ checkSections sec = topBindings helper
                                 { _projectionConstructor = headConstr,
                                   _projectionField = field ^. fieldName,
                                   _projectionFieldIx = idx,
-                                  _projectionFieldBuiltin = field ^. fieldBuiltin
+                                  _projectionFieldBuiltin = field ^. fieldBuiltin,
+                                  _projectionDoc = field ^. fieldDoc,
+                                  _projectionPragmas = field ^. fieldPragmas
                                 }
 
                             getFields :: Sem (Fail ': s') [RecordStatement 'Parsed]
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 6e13d36b9c..00c7afc572 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -1429,6 +1429,8 @@ rhsGadt = P.label "<constructor gadt>" $ do
 
 recordField :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RecordField 'Parsed)
 recordField = do
+  _fieldDoc <- optional stashJudoc >> getJudoc
+  _fieldPragmas <- optional stashPragmas >> getPragmas
   _fieldBuiltin <- optional builtinRecordField
   _fieldName <- symbol
   _fieldColon <- Irrelevant <$> kw kwColon
diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs
index fe8c544897..b35300824d 100644
--- a/src/Juvix/Compiler/Internal/Extra.hs
+++ b/src/Juvix/Compiler/Internal/Extra.hs
@@ -99,10 +99,11 @@ genFieldProjection ::
   (Members '[NameIdGen] r) =>
   FunctionName ->
   Maybe BuiltinFunction ->
+  Maybe Pragmas ->
   ConstructorInfo ->
   Int ->
   Sem r FunctionDef
-genFieldProjection _funDefName _funDefBuiltin info fieldIx = do
+genFieldProjection _funDefName _funDefBuiltin mpragmas info fieldIx = do
   body' <- genBody
   let (inductiveParams, constrArgs) = constructorArgTypes info
       implicity = constructorImplicity info
@@ -115,7 +116,11 @@ genFieldProjection _funDefName _funDefBuiltin info fieldIx = do
         _funDefInstance = False,
         _funDefCoercion = False,
         _funDefArgsInfo = mempty,
-        _funDefPragmas = mempty {_pragmasInline = Just InlineAlways},
+        _funDefPragmas =
+          maybe
+            (mempty {_pragmasInline = Just InlineAlways})
+            (over pragmasInline (maybe (Just InlineAlways) Just))
+            mpragmas,
         _funDefBody = body',
         _funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy,
         _funDefName,
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 685d3bb45f..a0c333b487 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -352,7 +352,7 @@ goProjectionDef ::
 goProjectionDef ProjectionDef {..} = do
   let c = goSymbol _projectionConstructor
   info <- gets (^?! constructorInfos . at c . _Just)
-  fun <- Internal.genFieldProjection (goSymbol _projectionField) ((^. withLocParam) <$> _projectionFieldBuiltin) info _projectionFieldIx
+  fun <- Internal.genFieldProjection (goSymbol _projectionField) ((^. withLocParam) <$> _projectionFieldBuiltin) (fmap (^. withLocParam . withSourceValue) _projectionPragmas) info _projectionFieldIx
   whenJust (fun ^. Internal.funDefBuiltin) (registerBuiltinFunction fun)
   return fun
 
diff --git a/tests/positive/Format.juvix b/tests/positive/Format.juvix
index ccaf0fa5c8..133fbcfeee 100644
--- a/tests/positive/Format.juvix
+++ b/tests/positive/Format.juvix
@@ -354,6 +354,17 @@ module OperatorRecord;
     in n + m * m;
 end;
 
+module RecordFieldPragmas;
+  type Pr (A B : Type) :=
+    mkPr {
+      --- Judoc for A
+      {-# inline: false #-}
+      pfst : A;
+      {-# inline: false #-}
+      psnd : B
+    };
+end;
+
 longLongLongArg : Int := 0;
 
 longLongLongListArg : List Int := [];