chore: remove <$ and $> notation

cc @Kha

src/Init/Control/Functor.lean

@@ -13,17 +13,12 @@ class Functor (f : Type u → Type v) : Type (max (u+1) v) :=
 (mapConst : ∀ {α β : Type u}, α → f β → f α := fun α β => map ∘ const β)
 
 infixr `<$>` := Functor.map
-infixr `<$`  := Functor.mapConst
-
-@[reducible] def Functor.mapConstRev {f : Type u → Type v} [Functor f] {α β : Type u} : f β → α → f α :=
-fun a b => b <$ a
-infixr `$>`  := Functor.mapConstRev
 
 @[reducible] def Functor.mapRev {f : Type u → Type v} [Functor f] {α β : Type u} : f α → (α → β) → f β :=
 fun a f => f <$> a
 infixl `<&>` := Functor.mapRev
 
 def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) : f PUnit :=
-PUnit.unit <$ x
+Functor.mapConst PUnit.unit x
 
 export Functor (discard)

src/Init/Core.lean

@@ -73,8 +73,6 @@ reserve infixl ` <* ` :60
 reserve infixr ` *> ` :60
 reserve infixr ` >> ` :60
 reserve infixr ` <$> `:100
-reserve infixr ` <$ ` :100
-reserve infixr ` $> ` :100
 reserve infixl ` <&> `:100
 
 universes u v w

src/Lean/Elab/BuiltinNotation.lean

@@ -241,8 +241,6 @@ fun stx => elabInfix (mkCTermIdFrom (stx.getArg 1) op) stx
 
 @[builtinMacro Lean.Parser.Term.map] def elabMap : Macro := elabInfixOp `Functor.map
 @[builtinMacro Lean.Parser.Term.mapRev] def elabMapRev : Macro := elabInfixOp `Functor.mapRev
-@[builtinMacro Lean.Parser.Term.mapConst] def elabMapConst : Macro := elabInfixOp `Functor.mapConst
-@[builtinMacro Lean.Parser.Term.mapConstRev] def elabMapConstRev : Macro := elabInfixOp `Functor.mapConstRev
 
 @[builtinMacro Lean.Parser.Term.orelse] def elabOrElse : Macro := elabInfixOp `HasOrelse.orelse
 @[builtinMacro Lean.Parser.Term.orM] def elabOrM : Macro := elabInfixOp `orM

src/Lean/Parser/Term.lean

@@ -203,8 +203,6 @@ def namedArgument  := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
 @[builtinTermParser] def seqLeft     := tparser! infixL " <* "  60
 @[builtinTermParser] def seqRight    := tparser! infixR " *> "  60
 @[builtinTermParser] def map         := tparser! infixR " <$> " 100
-@[builtinTermParser] def mapConst    := tparser! infixR " <$ "  100
-@[builtinTermParser] def mapConstRev := tparser! infixR " $> "  100
 
 @[builtinTermParser] def tacticBlock := parser! "begin " >> Tactic.seq >> "end"
 @[builtinTermParser] def byTactic    := parser!:leadPrec "by " >> Tactic.nonEmptySeq