diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 5da2743c25..e45a4c0dcb 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -363,7 +363,7 @@ def funBinder : Parser :=
 -- NOTE: we disable anonymous antiquotations to ensure that `fun $b => ...`
 -- remains a `term` antiquotation
 def basicFun : Parser := leading_parser (withAnonymousAntiquot := false)
-  ppGroup (many1 (ppSpace >> funBinder) >> optType >> " =>") >> ppSpace >> termParser
+  ppGroup (many1 (ppSpace >> funBinder) >> optType >> unicodeSymbol " ↦" " =>") >> ppSpace >> termParser
 @[builtin_term_parser] def «fun» := leading_parser:maxPrec
   ppAllowUngrouped >> unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts)
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 0ee5849edd..a753239408 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -520,9 +520,14 @@ def delabLam : Delab :=
         | BinderInfo.instImplicit,   _     =>
           if usedDownstream then `(funBinder| [$curNames.back : $stxT])  -- here `curNames.size == 1`
           else  `(funBinder| [$stxT])
-      match stxBody with
-      | `(fun $binderGroups* => $stxBody) => `(fun $group $binderGroups* => $stxBody)
-      | _                                 => `(fun $group => $stxBody)
+      let (binders, stxBody) :=
+        match stxBody with
+        | `(fun $binderGroups* => $stxBody) => (#[group] ++ binderGroups, stxBody)
+        | _                                 => (#[group], stxBody)
+      if ← getPPOption getPPUnicodeFun then
+        `(fun $binders* ↦ $stxBody)
+      else
+        `(fun $binders* => $stxBody)
 
 /--
 Similar to `delabBinders`, but tracking whether `forallE` is dependent or not.
diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean
index 4249c7f2fd..764bbc0084 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Options.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean
@@ -18,6 +18,11 @@ register_builtin_option pp.notation : Bool := {
   group    := "pp"
   descr    := "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)"
 }
+register_builtin_option pp.unicode.fun : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) disable/enable unicode ↦ notation for functions"
+}
 register_builtin_option pp.match : Bool := {
   defValue := true
   group    := "pp"
@@ -181,6 +186,7 @@ def getPPLetVarTypes (o : Options) : Bool := o.get pp.letVarTypes.name (getPPAll
 def getPPCoercions (o : Options) : Bool := o.get pp.coercions.name (!getPPAll o)
 def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o)
 def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o)
+def getPPUnicodeFun (o : Options) : Bool := o.get pp.unicode.fun.name false
 def getPPMatch (o : Options) : Bool := o.get pp.match.name (!getPPAll o)
 def getPPStructureProjections (o : Options) : Bool := o.get pp.structureProjections.name (!getPPAll o)
 def getPPStructureInstances (o : Options) : Bool := o.get pp.structureInstances.name (!getPPAll o)
diff --git a/tests/lean/ppUnicode.lean b/tests/lean/ppUnicode.lean
new file mode 100644
index 0000000000..19919ff9cd
--- /dev/null
+++ b/tests/lean/ppUnicode.lean
@@ -0,0 +1,5 @@
+#check fun a b c ↦  a + b + c + 1
+set_option pp.unicode.fun true in
+#check fun a b c => a + b + c + 1
+set_option pp.unicode.fun true in
+#check ∃ n : Nat, n ≤ 0
diff --git a/tests/lean/ppUnicode.lean.expected.out b/tests/lean/ppUnicode.lean.expected.out
new file mode 100644
index 0000000000..79fe9d00ff
--- /dev/null
+++ b/tests/lean/ppUnicode.lean.expected.out
@@ -0,0 +1,3 @@
+fun a b c => a + b + c + 1 : Nat → Nat → Nat → Nat
+fun a b c ↦ a + b + c + 1 : Nat → Nat → Nat → Nat
+∃ n, n ≤ 0 : Prop