feat: add mapsTo syntax

src/Lean/Meta/Basic.lean

@@ -34,22 +34,22 @@ namespace Lean.Meta
 builtin_initialize isDefEqStuckExceptionId : InternalExceptionId ← registerInternalExceptionId `isDefEqStuck
 
 /--
-  Configuration flags for the `MetaM` monad.
-  Many of them are used to control the `isDefEq` function that checks whether two terms are definitionally equal or not.
-  Recall that when `isDefEq` is trying to check whether
-  `?m@C a₁ ... aₙ` and `t` are definitionally equal (`?m@C a₁ ... aₙ =?= t`), where
-  `?m@C` as a shorthand for `C |- ?m : t` where `t` is the type of `?m`.
-  We solve it using the assignment `?m := fun a₁ ... aₙ => t` if
-  1) `a₁ ... aₙ` are pairwise distinct free variables that are ​*not*​ let-variables.
-  2) `a₁ ... aₙ` are not in `C`
-  3) `t` only contains free variables in `C` and/or `{a₁, ..., aₙ}`
-  4) For every metavariable `?m'@C'` occurring in `t`, `C'` is a subprefix of `C`
-  5) `?m` does not occur in `t`
+Configuration flags for the `MetaM` monad.
+Many of them are used to control the `isDefEq` function that checks whether two terms are definitionally equal or not.
+Recall that when `isDefEq` is trying to check whether
+`?m@C a₁ ... aₙ` and `t` are definitionally equal (`?m@C a₁ ... aₙ =?= t`), where
+`?m@C` as a shorthand for `C |- ?m : t` where `t` is the type of `?m`.
+We solve it using the assignment `?m := fun a₁ ... aₙ => t` if
+1) `a₁ ... aₙ` are pairwise distinct free variables that are ​*not*​ let-variables.
+2) `a₁ ... aₙ` are not in `C`
+3) `t` only contains free variables in `C` and/or `{a₁, ..., aₙ}`
+4) For every metavariable `?m'@C'` occurring in `t`, `C'` is a subprefix of `C`
+5) `?m` does not occur in `t`
 -/
 structure Config where
   /--
     If `foApprox` is set to true, and some `aᵢ` is not a free variable,
-     then we use first-order unification
+    then we use first-order unification
      ```
        ?m a_1 ... a_i a_{i+1} ... a_{i+k} =?= f b_1 ... b_k
      ```

src/Lean/Meta/ExprDefEq.lean

@@ -1333,15 +1333,6 @@ private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do
   if tArgs.size < fvars.size then return none
   return some (mkAppRange (mkMVar mvarIdPending) fvars.size tArgs.size tArgs)
 
-private def isSynthetic : Expr → MetaM Bool
-  | Expr.mvar mvarId => do
-    let mvarDecl ← getMVarDecl mvarId
-    match mvarDecl.kind with
-    | MetavarKind.synthetic       => pure true
-    | MetavarKind.syntheticOpaque => pure true
-    | MetavarKind.natural         => pure false
-  | _                  => pure false
-
 private def isAssignable : Expr → MetaM Bool
   | Expr.mvar mvarId => do let b ← isReadOnlyOrSyntheticOpaqueExprMVar mvarId; pure (!b)
   | _                => pure false

src/Lean/Parser/Term.lean

@@ -131,6 +131,8 @@ Note that we did not add a `explicitShortBinder` parser since `(α) → α →
 -/
 @[builtinTermParser] def depArrow := leading_parser:25 bracketedBinder true >> unicodeSymbol " → " " -> " >> termParser
 
+@[builtinTermParser] def mapsTo := leading_parser:25 bracketedBinder true >> unicodeSymbol " ↦ " " |-> " >> termParser
+
 @[builtinTermParser]
 def «forall» := leading_parser:leadPrec unicodeSymbol "∀" "forall" >> many1 (ppSpace >> (binderIdent <|> bracketedBinder)) >> optType >> ", " >> termParser