more inline

Author: datokrat

src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean

@@ -114,7 +114,7 @@ This combinator incurs an additional O(1) cost with each output of `it` or an in
 
 For each value emitted by the outer iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, expose]
+@[always_inline, inline, expose]
 public def IterM.flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
     (f : β → m (IterM (α := α₂) m γ)) (it : IterM (α := α) m β) :=
@@ -195,7 +195,7 @@ This combinator incurs an additional O(1) cost with each output of `it` or an in
 
 For each value emitted by the outer iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, expose]
+@[always_inline, inline, expose]
 public def IterM.flatMap {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
     (f : β → IterM (α := α₂) m γ) (it : IterM (α := α) m β) :=

src/Init/Data/Iterators/Consumers/Loop.lean

@@ -240,12 +240,12 @@ def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id
     (it : Iter.Partial (α := α) β) (f : β → Bool) : Option β :=
   it.it.find? f
 
-@[always_inline, expose, inherit_doc IterM.size]
+@[always_inline, inline, expose, inherit_doc IterM.size]
 def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
     (it : Iter (α := α) β) : Nat :=
   (IteratorSize.size it.toIterM).run.down
 
-@[always_inline, inherit_doc IterM.Partial.size]
+@[always_inline, inline, inherit_doc IterM.Partial.size]
 def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSizePartial α Id]
     (it : Iter (α := α) β) : Nat :=
   (IteratorSizePartial.size it.toIterM).run.down

src/Init/Data/Iterators/Consumers/Monadic/Loop.lean

@@ -114,7 +114,7 @@ instance IteratorLoop.WithWF.instWellFoundedRelation
 /--
 This is the loop implementation of the default instance `IteratorLoop.defaultImplementation`.
 -/
-@[always_inline, expose]
+@[always_inline, inline, expose]
 def IterM.DefaultConsumers.forIn' {m : Type w → Type w'} {α : Type w} {β : Type w}
     [Iterator α m β]
     {n : Type x → Type x'} [Monad n]
@@ -169,7 +169,7 @@ This is the default implementation of the `IteratorLoop` class.
 It simply iterates through the iterator using `IterM.step`. For certain iterators, more efficient
 implementations are possible and should be used instead.
 -/
-@[always_inline, expose]
+@[always_inline, inline, expose]
 def IteratorLoop.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type x → Type x'}
     [Monad n] [Iterator α m β] :
     IteratorLoop α m n where