diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index f557f93e98..3f2530b694 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -277,6 +277,17 @@ end Delaborator
 open SubExpr (Pos PosMap)
 open Delaborator (OptionsPerPos topDownAnalyze)
 
+/-- Custom version of `Lean.Core.betaReduce` to beta reduce expressions for the `pp.beta` option.
+We do not want to beta reduce the application in `let_fun` annotations. -/
+private partial def betaReduce' (e : Expr) : CoreM Expr :=
+  Core.transform e (pre := fun e => do
+    if isLetFun e then
+      return .done <| e.updateMData! (.app (← betaReduce' e.mdataExpr!.appFn!) (← betaReduce' e.mdataExpr!.appArg!))
+    else if e.isHeadBetaTarget then
+      return .visit e.headBeta
+    else
+      return .continue)
+
 def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (Term × PosMap Elab.Info) := do
   /- Using `erasePatternAnnotations` here is a bit hackish, but we do it
      `Expr.mdata` affects the delaborator. TODO: should we fix that? -/
@@ -291,6 +302,7 @@ def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delabor
     catch _ => pure ()
   withOptions (fun _ => opts) do
     let e ← if getPPInstantiateMVars opts then instantiateMVars e else pure e
+    let e ← if getPPBeta opts then betaReduce' e else pure e
     let optionsPerPos ←
       if !getPPAll opts && getPPAnalyze opts && optionsPerPos.isEmpty then
         topDownAnalyze e
diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean
index 764bbc0084..c9d5e0a384 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Options.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean
@@ -68,6 +68,11 @@ register_builtin_option pp.instantiateMVars : Bool := {
   group    := "pp"
   descr    := "(pretty printer) instantiate mvars before delaborating"
 }
+register_builtin_option pp.beta : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) apply beta-reduction when pretty printing"
+}
 register_builtin_option pp.structureInstances : Bool := {
   defValue := true
   group    := "pp"
@@ -152,11 +157,6 @@ register_builtin_option g_pp_locals_full_names : Bool := {
   group    := "pp"
   descr    := "(pretty printer) show full names of locals"
 }
-register_builtin_option g_pp_beta : Bool := {
-  defValue := false
-  group    := "pp"
-  descr    := "(pretty printer) apply beta-reduction when pretty printing"
-}
 register_builtin_option g_pp_goal_compact : Bool := {
   defValue := false
   group    := "pp"
@@ -196,6 +196,7 @@ def getPPUniverses (o : Options) : Bool := o.get pp.universes.name (getPPAll o)
 def getPPFullNames (o : Options) : Bool := o.get pp.fullNames.name (getPPAll o)
 def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPAll o)
 def getPPInstantiateMVars (o : Options) : Bool := o.get pp.instantiateMVars.name pp.instantiateMVars.defValue
+def getPPBeta (o : Options) : Bool := o.get pp.beta.name pp.beta.defValue
 def getPPSafeShadowing (o : Options) : Bool := o.get pp.safeShadowing.name pp.safeShadowing.defValue
 def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (getPPAll o)
 def getPPProofsWithType (o : Options) : Bool := o.get pp.proofs.withType.name pp.proofs.withType.defValue
diff --git a/tests/lean/ppBeta.lean b/tests/lean/ppBeta.lean
new file mode 100644
index 0000000000..44fe8f2fda
--- /dev/null
+++ b/tests/lean/ppBeta.lean
@@ -0,0 +1,13 @@
+#check (fun x => x) Nat
+
+#check let_fun x := Nat; x
+
+set_option pp.beta true
+
+#check (fun x => x) Nat
+
+#check let_fun x := Nat; x
+
+set_option pp.all true
+
+#check (fun x => x) Nat
diff --git a/tests/lean/ppBeta.lean.expected.out b/tests/lean/ppBeta.lean.expected.out
new file mode 100644
index 0000000000..351e60c62d
--- /dev/null
+++ b/tests/lean/ppBeta.lean.expected.out
@@ -0,0 +1,7 @@
+(fun x => x) Nat : Type
+let_fun x := Nat;
+x : Type
+Nat : Type
+let_fun x := Nat;
+x : Type
+Nat : Type