From 75243e7f244f096aa05ea965a463e7ee46c5830d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 12 Feb 2021 10:57:41 +0100 Subject: [PATCH] feat: change back `seqLeft/Right` signature This was originally changed for the sake of `do`, which does not depend on it anymore --- src/Init/Prelude.lean | 6 +++--- tests/lean/run/struct3.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 3cde822aa9..436c032638 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1122,10 +1122,10 @@ class Seq (f : Type u → Type v) : Type (max (u+1) v) where seq : {α β : Type u} → f (α → β) → f α → f β class SeqLeft (f : Type u → Type v) : Type (max (u+1) v) where - seqLeft : {α : Type u} → f α → f PUnit → f α + seqLeft : {α β : Type u} → f α → f β → f α class SeqRight (f : Type u → Type v) : Type (max (u+1) v) where - seqRight : {β : Type u} → f PUnit → f β → f β + seqRight : {α β : Type u} → f α → f β → f β class Applicative (f : Type u → Type v) extends Functor f, Pure f, Seq f, SeqLeft f, SeqRight f where map := fun x y => Seq.seq (pure x) y @@ -1468,7 +1468,7 @@ class Backtrackable (δ : outParam (Type u)) (σ : Type u) where | Result.ok a s => Result.ok (f a) s | Result.error e s => Result.error e s -@[inline] protected def seqRight (x : EStateM ε σ PUnit) (y : EStateM ε σ β) : EStateM ε σ β := fun s => +@[inline] protected def seqRight (x : EStateM ε σ α) (y : EStateM ε σ β) : EStateM ε σ β := fun s => match x s with | Result.ok _ s => y s | Result.error e s => Result.error e s diff --git a/tests/lean/run/struct3.lean b/tests/lean/run/struct3.lean index 28e227373b..3879aa5cc3 100644 --- a/tests/lean/run/struct3.lean +++ b/tests/lean/run/struct3.lean @@ -7,7 +7,7 @@ class Monad2 (m : Type u → Type v) extends Applicative m, Bind2 m : Type (max map := fun f x => Bind2.bind x (pure ∘ f) seq := fun f x => Bind2.bind f fun y => Functor.map y x seqLeft := fun x y => Bind2.bind x fun a => Bind2.bind y fun _ => pure a - seqRight := @fun β x y => Bind2.bind x fun _ => y -- Recall that `@` disables implicit lambda support + seqRight := @fun α β x y => Bind2.bind x fun _ => y -- Recall that `@` disables implicit lambda support class Monad3 (m : Type u → Type v) extends Applicative m, Bind2 m : Type (max (u+1) v) where map (f x) := Bind2.bind x (pure ∘ f)