From d3e225ec65935990c4210017641a25affe033c36 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Sep 2018 21:42:22 -0700
Subject: [PATCH] fix(library/init): missing `@[inline]`

---
 library/init/coe.lean           | 16 ++++++++--------
 library/init/control/state.lean |  4 ++--
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/library/init/coe.lean b/library/init/coe.lean
index ccd4c6e2b9..1cc7c3ea02 100644
--- a/library/init/coe.lean
+++ b/library/init/coe.lean
@@ -47,30 +47,30 @@ class has_coe_to_fun (a : Sort u) : Sort (max u (v+1)) :=
 class has_coe_to_sort (a : Sort u) : Type (max u (v+1)) :=
 (S : Sort v) (coe : a → S)
 
-def lift {a : Sort u} {b : Sort v} [has_lift a b] : a → b :=
+@[inline] def lift {a : Sort u} {b : Sort v} [has_lift a b] : a → b :=
 @has_lift.lift a b _
 
-def lift_t {a : Sort u} {b : Sort v} [has_lift_t a b] : a → b :=
+@[inline] def lift_t {a : Sort u} {b : Sort v} [has_lift_t a b] : a → b :=
 @has_lift_t.lift a b _
 
-def coe_b {a : Sort u} {b : Sort v} [has_coe a b] : a → b :=
+@[inline] def coe_b {a : Sort u} {b : Sort v} [has_coe a b] : a → b :=
 @has_coe.coe a b _
 
-def coe_t {a : Sort u} {b : Sort v} [has_coe_t a b] : a → b :=
+@[inline] def coe_t {a : Sort u} {b : Sort v} [has_coe_t a b] : a → b :=
 @has_coe_t.coe a b _
 
-def coe_fn_b {a : Sort u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
+@[inline] def coe_fn_b {a : Sort u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
 has_coe_to_fun.coe
 
 /- User level coercion operators -/
 
-@[reducible] def coe {a : Sort u} {b : Sort v} [has_lift_t a b] : a → b :=
+@[reducible, inline] def coe {a : Sort u} {b : Sort v} [has_lift_t a b] : a → b :=
 lift_t
 
-@[reducible] def coe_fn {a : Sort u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
+@[reducible, inline] def coe_fn {a : Sort u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
 has_coe_to_fun.coe
 
-@[reducible] def coe_sort {a : Sort u} [has_coe_to_sort.{u v} a] : a → has_coe_to_sort.S.{u v} a :=
+@[reducible, inline] def coe_sort {a : Sort u} [has_coe_to_sort.{u v} a] : a → has_coe_to_sort.S.{u v} a :=
 has_coe_to_sort.coe
 
 /- Notation -/
diff --git a/library/init/control/state.lean b/library/init/control/state.lean
index 881a35492f..e0da06a931 100644
--- a/library/init/control/state.lean
+++ b/library/init/control/state.lean
@@ -34,10 +34,10 @@ section
   instance : monad (state_t σ m) :=
   { pure := @state_t.pure _ _ _, bind := @state_t.bind _ _ _ }
 
-  protected def orelse [alternative m] {α : Type u} (x₁ x₂ : state_t σ m α) : state_t σ m α :=
+  @[inline] protected def orelse [alternative m] {α : Type u} (x₁ x₂ : state_t σ m α) : state_t σ m α :=
   ⟨λ s, x₁.run s <|> x₂.run s⟩
 
-  protected def failure [alternative m] {α : Type u} : state_t σ m α :=
+  @[inline] protected def failure [alternative m] {α : Type u} : state_t σ m α :=
   ⟨λ s, failure⟩
 
   instance [alternative m] : alternative (state_t σ m) :=