diff --git a/src/Init/Control/Functor.lean b/src/Init/Control/Functor.lean index af4a5259bc..2dc6de4547 100644 --- a/src/Init/Control/Functor.lean +++ b/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) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index c6631f2516..ac4b615a14 100644 --- a/src/Init/Core.lean +++ b/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 diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index ad2ee31ddb..16bd025643 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/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 diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index db67cad66d..8047ff8275 100644 --- a/src/Lean/Parser/Term.lean +++ b/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