feat: add fun x ↦ y syntax

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)
 

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.

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)

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

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