max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: <&>

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-01 13:55:59 +01:00 • committed by Leonardo de Moura
parent 07f25a19db
commit 1f9e8bc93d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Control/Basic.lean
View file

@ -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