From 1f9e8bc93d4fffaef11475bffa7fc243cf4395a6 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 1 Dec 2020 13:55:59 +0100 Subject: [PATCH] fix: <&> --- src/Init/Control/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean index 5dc56cb45f..1dca06d9cb 100644 --- a/src/Init/Control/Basic.lean +++ b/src/Init/Control/Basic.lean @@ -11,7 +11,7 @@ universes u v w @[reducible] def Functor.mapRev {f : Type u → Type v} [Functor f] {α β : Type u} : f α → (α → β) → f β := fun a f => f <$> a -infixr:100 " <&> " => Fuctor.mapRev +infixr:100 " <&> " => Functor.mapRev def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) : f PUnit := Functor.mapConst PUnit.unit x