From 741fac924a193be309c03f36eb015f9a08240ce7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 15 Oct 2022 13:04:55 +0200 Subject: [PATCH] chore: inline control primitives --- src/Init/Control/Basic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean index a1090331b9..0ee7148863 100644 --- a/src/Init/Control/Basic.lean +++ b/src/Init/Control/Basic.lean @@ -233,14 +233,17 @@ class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂)) export ForM (forM) /-- Left-to-right composition of Kleisli arrows. -/ +@[alwaysInline] def Bind.kleisliRight [Bind m] (f₁ : α → m β) (f₂ : β → m γ) (a : α) : m γ := f₁ a >>= f₂ /-- Right-to-left composition of Kleisli arrows. -/ +@[alwaysInline] def Bind.kleisliLeft [Bind m] (f₂ : β → m γ) (f₁ : α → m β) (a : α) : m γ := f₁ a >>= f₂ /-- Same as `Bind.bind` but with arguments swapped. -/ +@[alwaysInline] def Bind.bindLeft [Bind m] (f : α → m β) (ma : m α) : m β := ma >>= f