From 0742fd6fc3b42fdbc7d2296f994ca7e578cb212b Mon Sep 17 00:00:00 2001 From: Juan Pablo Romero Date: Mon, 12 Sep 2022 22:43:59 -0700 Subject: [PATCH] docs: fix typo in SeqRight docstring --- src/Init/Prelude.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index b45809b457..09f13f5471 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -2610,7 +2610,7 @@ class SeqLeft (f : Type u → Type v) : Type (max (u+1) v) where `Unit → f β` function. -/ seqLeft : {α β : Type u} → f α → (Unit → f β) → f α -/-- The typeclass which supplies the `<*` "seqRight" function. See `Applicative`. -/ +/-- The typeclass which supplies the `*>` "seqRight" function. See `Applicative`. -/ class SeqRight (f : Type u → Type v) : Type (max (u+1) v) where /-- If `x : F α` and `y : F β`, then `x *> y` evaluates `x`, then `y`, and returns the result of `y`.