From a7069060f5f354acedb0b0d7b410a348e321cc0c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 30 Mar 2019 20:54:39 -0700 Subject: [PATCH] fix(library/init/control): camelCase conversion typos --- library/init/control/applicative.lean | 4 ++-- library/init/control/monad.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/library/init/control/applicative.lean b/library/init/control/applicative.lean index 3ca18e9f1b..fdc8cab991 100644 --- a/library/init/control/applicative.lean +++ b/library/init/control/applicative.lean @@ -14,9 +14,9 @@ class HasPure (f : Type u → Type v) := export HasPure (pure) class HasSeq (f : Type u → Type v) : Type (max (u+1) v) := -(Seq : Π {α β : Type u}, f (α → β) → f α → f β) +(seq : Π {α β : Type u}, f (α → β) → f α → f β) -infixl ` <*> `:60 := HasSeq.Seq +infixl ` <*> `:60 := HasSeq.seq class HasSeqLeft (f : Type u → Type v) : Type (max (u+1) v) := (seqLeft : Π {α β : Type u}, f α → f β → f α) diff --git a/library/init/control/monad.lean b/library/init/control/monad.lean index 9c4aa090c6..470ed76bfc 100644 --- a/library/init/control/monad.lean +++ b/library/init/control/monad.lean @@ -17,8 +17,8 @@ export HasBind (bind) infixl ` >>= `:55 := bind class Monad (m : Type u → Type v) extends Applicative m, HasBind m : Type (max (u+1) v) := -(map := λ α β f x, x >>= pure ∘ f) -(Seq := λ α β f x, f >>= (<$> x)) +(map := λ α β f x, x >>= pure ∘ f) +(seq := λ α β f x, f >>= (<$> x)) (seqLeft := λ α β x y, x >>= λ a, y >>= λ _, pure a) (seqRight := λ α β x y, x >>= λ _, y)