chore: snake-case attributes (part 2)

src/Init/Control/Basic.lean

@@ -14,7 +14,7 @@ def Functor.mapRev {f : Type u → Type v} [Functor f] {α β : Type u} : f α 
 
 infixr:100 " <&> " => Functor.mapRev
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) : f PUnit :=
   Functor.mapConst PUnit.unit x
 
@@ -30,10 +30,10 @@ variable {f : Type u → Type v} [Alternative f] {α : Type u}
 
 export Alternative (failure)
 
-@[alwaysInline, inline] def guard {f : Type → Type v} [Alternative f] (p : Prop) [Decidable p] : f Unit :=
+@[always_inline, inline] def guard {f : Type → Type v} [Alternative f] (p : Prop) [Decidable p] : f Unit :=
   if p then pure () else failure
 
-@[alwaysInline, inline] def optional (x : f α) : f (Option α) :=
+@[always_inline, inline] def optional (x : f α) : f (Option α) :=
   some <$> x <|> pure none
 
 class ToBool (α : Type u) where
@@ -44,28 +44,28 @@ export ToBool (toBool)
 instance : ToBool Bool where
   toBool b := b
 
-@[macroInline] def bool {β : Type u} {α : Type v} [ToBool β] (f t : α) (b : β) : α :=
+@[macro_inline] def bool {β : Type u} {α : Type v} [ToBool β] (f t : α) (b : β) : α :=
   match toBool b with
   | true  => t
   | false => f
 
-@[macroInline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
+@[macro_inline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
   let b ← x
   match toBool b with
   | true  => pure b
   | false => y
 
 infixr:30 " <||> " => orM
 
-@[macroInline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
+@[macro_inline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
   let b ← x
   match toBool b with
   | true  => y
   | false => pure b
 
 infixr:35 " <&&> " => andM
 
-@[macroInline] def notM {m : Type → Type v} [Applicative m] (x : m Bool) : m Bool :=
+@[macro_inline] def notM {m : Type → Type v} [Applicative m] (x : m Bool) : m Bool :=
   not <$> x
 
 /-!
@@ -199,7 +199,7 @@ class MonadControlT (m : Type u → Type v) (n : Type u → Type w) where
 
 export MonadControlT (stM liftWith restoreM)
 
-@[alwaysInline]
+@[always_inline]
 instance (m n o) [MonadControl n o] [MonadControlT m n] : MonadControlT m o where
   stM α := stM m n (MonadControl.stM n o α)
   liftWith f := MonadControl.liftWith fun x₂ => liftWith fun x₁ => f (x₁ ∘ x₂)
@@ -210,12 +210,12 @@ instance (m : Type u → Type v) [Pure m] : MonadControlT m m where
   liftWith f := f fun x => x
   restoreM x := pure x
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 def controlAt (m : Type u → Type v) {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u}
     (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α :=
   liftWith f >>= restoreM
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 def control {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u}
     (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α :=
   controlAt m f
@@ -233,22 +233,22 @@ class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂))
 export ForM (forM)
 
 /-- Left-to-right composition of Kleisli arrows. -/
-@[alwaysInline]
+@[always_inline]
 def Bind.kleisliRight [Bind m] (f₁ : α → m β) (f₂ : β → m γ) (a : α) : m γ :=
   f₁ a >>= f₂
 
 /-- Right-to-left composition of Kleisli arrows. -/
-@[alwaysInline]
+@[always_inline]
 def Bind.kleisliLeft [Bind m] (f₂ : β → m γ) (f₁ : α → m β) (a : α) : m γ :=
   f₁ a >>= f₂
 
 /-- Same as `Bind.bind` but with arguments swapped. -/
-@[alwaysInline]
+@[always_inline]
 def Bind.bindLeft [Bind m] (f : α → m β) (ma : m α) : m β :=
   ma >>= f
 
 -- Precedence choice taken to be the same as in haskell:
 -- https://hackage.haskell.org/package/base-4.17.0.0/docs/Control-Monad.html#v:-61--60--60-
-@[inheritDoc] infixr:55 " >=> " => Bind.kleisliRight
-@[inheritDoc] infixr:55 " <=< " => Bind.kleisliLeft
-@[inheritDoc] infixr:55 " =<< " => Bind.bindLeft
+@[inherit_doc] infixr:55 " >=> " => Bind.kleisliRight
+@[inherit_doc] infixr:55 " <=< " => Bind.kleisliLeft
+@[inherit_doc] infixr:55 " =<< " => Bind.bindLeft

src/Init/Control/EState.lean

@@ -31,7 +31,7 @@ variable {ε σ α β : Type u}
 
 /-- Alternative orElse operator that allows to select which exception should be used.
     The default is to use the first exception since the standard `orElse` uses the second. -/
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def orElse' {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (useFirstEx := true) : EStateM ε σ α := fun s =>
   let d := Backtrackable.save s;
   match x₁ s with
@@ -41,7 +41,7 @@ protected def orElse' {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α)
     | ok                 => ok
   | ok                 => ok
 
-@[alwaysInline]
+@[always_inline]
 instance : MonadFinally (EStateM ε σ) := {
   tryFinally' := fun x h s =>
     let r := x s
@@ -54,7 +54,7 @@ instance : MonadFinally (EStateM ε σ) := {
       | Result.error e₂ s => Result.error e₂ s
 }
 
-@[alwaysInline, inline] def fromStateM {ε σ α : Type} (x : StateM σ α) : EStateM ε σ α := fun s =>
+@[always_inline, inline] def fromStateM {ε σ α : Type} (x : StateM σ α) : EStateM ε σ α := fun s =>
   match x.run s with
   | (a, s') => EStateM.Result.ok a s'
 

src/Init/Control/Except.lean

@@ -13,11 +13,11 @@ import Init.Coe
 namespace Except
 variable {ε : Type u}
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def pure (a : α) : Except ε α :=
   Except.ok a
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def map (f : α → β) : Except ε α → Except ε β
   | Except.error err => Except.error err
   | Except.ok v => Except.ok <| f v
@@ -27,31 +27,31 @@ protected def map (f : α → β) : Except ε α → Except ε β
   intro e
   simp [Except.map]; cases e <;> rfl
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def mapError (f : ε → ε') : Except ε α → Except ε' α
   | Except.error err => Except.error <| f err
   | Except.ok v      => Except.ok v
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def bind (ma : Except ε α) (f : α → Except ε β) : Except ε β :=
   match ma with
   | Except.error err => Except.error err
   | Except.ok v      => f v
 
 /-- Returns true if the value is `Except.ok`, false otherwise. -/
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def toBool : Except ε α → Bool
   | Except.ok _    => true
   | Except.error _ => false
 
 abbrev isOk : Except ε α → Bool := Except.toBool
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def toOption : Except ε α → Option α
   | Except.ok a    => some a
   | Except.error _ => none
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def tryCatch (ma : Except ε α) (handle : ε → Except ε α) : Except ε α :=
   match ma with
   | Except.ok a    => Except.ok a
@@ -62,7 +62,7 @@ def orElseLazy (x : Except ε α) (y : Unit → Except ε α) : Except ε α :=
   | Except.ok a    => Except.ok a
   | Except.error _ => y ()
 
-@[alwaysInline]
+@[always_inline]
 instance : Monad (Except ε) where
   pure := Except.pure
   bind := Except.bind
@@ -73,69 +73,69 @@ end Except
 def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
   m (Except ε α)
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) : ExceptT ε m α := x
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α) := x
 
 namespace ExceptT
 
 variable {ε : Type u} {m : Type u → Type v} [Monad m]
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def pure {α : Type u} (a : α) : ExceptT ε m α :=
   ExceptT.mk <| pure (Except.ok a)
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def bindCont {α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)
   | Except.ok a    => f a
   | Except.error e => pure (Except.error e)
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def bind {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β :=
   ExceptT.mk <| ma >>= ExceptT.bindCont f
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def map {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β :=
   ExceptT.mk <| x >>= fun a => match a with
     | (Except.ok a)    => pure <| Except.ok (f a)
     | (Except.error e) => pure <| Except.error e
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def lift {α : Type u} (t : m α) : ExceptT ε m α :=
   ExceptT.mk <| Except.ok <$> t
 
-@[alwaysInline]
+@[always_inline]
 instance : MonadLift (Except ε) (ExceptT ε m) := ⟨fun e => ExceptT.mk <| pure e⟩
 instance : MonadLift m (ExceptT ε m) := ⟨ExceptT.lift⟩
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def tryCatch {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α :=
   ExceptT.mk <| ma >>= fun res => match res with
    | Except.ok a    => pure (Except.ok a)
    | Except.error e => (handle e)
 
 instance : MonadFunctor m (ExceptT ε m) := ⟨fun f x => f x⟩
 
-@[alwaysInline]
+@[always_inline]
 instance : Monad (ExceptT ε m) where
   pure := ExceptT.pure
   bind := ExceptT.bind
   map  := ExceptT.map
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m α := fun x =>
   ExceptT.mk <| Except.mapError f <$> x
 
 end ExceptT
 
-@[alwaysInline]
+@[always_inline]
 instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
   throw e := ExceptT.mk <| throwThe ε₁ e
   tryCatch x handle := ExceptT.mk <| tryCatchThe ε₁ x handle
 
-@[alwaysInline]
+@[always_inline]
 instance (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) where
   throw e := ExceptT.mk <| pure (Except.error e)
   tryCatch := ExceptT.tryCatch
@@ -152,13 +152,13 @@ variable {ε : Type u} {m : Type v → Type w}
 
 /-- Alternative orelse operator that allows to select which exception should be used.
     The default is to use the first exception since the standard `orelse` uses the second. -/
-@[alwaysInline, inline]
+@[always_inline, inline]
 def orelse' [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx := true) : m α :=
   tryCatch t₁ fun e₁ => tryCatch t₂ fun e₂ => throw (if useFirstEx then e₁ else e₂)
 
 end MonadExcept
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 def observing {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) : m (Except ε α) :=
   tryCatch (do let a ← x; pure (Except.ok a)) (fun ex => pure (Except.error ex))
 
@@ -182,19 +182,19 @@ class MonadFinally (m : Type u → Type v) where
 export MonadFinally (tryFinally')
 
 /-- Execute `x` and then execute `finalizer` even if `x` threw an exception -/
-@[alwaysInline, inline]
+@[always_inline, inline]
 def tryFinally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α :=
   let y := tryFinally' x (fun _ => finalizer)
   (·.1) <$> y
 
-@[alwaysInline]
+@[always_inline]
 instance Id.finally : MonadFinally Id where
   tryFinally' := fun x h =>
    let a := x
    let b := h (some x)
    pure (a, b)
 
-@[alwaysInline]
+@[always_inline]
 instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] : MonadFinally (ExceptT ε m) where
   tryFinally' := fun x h => ExceptT.mk do
     let r ← tryFinally' x fun e? => match e? with

src/Init/Control/ExceptCps.lean

@@ -14,19 +14,19 @@ def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type
 
 namespace ExceptCpsT
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 def run {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) : m (Except ε α) :=
   x _ (fun a => pure (Except.ok a)) (fun e => pure (Except.error e))
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 def runK {ε α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : α → m β) (error : ε → m β) : m β :=
   x _ ok error
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 def runCatch [Monad m] (x : ExceptCpsT α m α) : m α :=
   x α pure pure
 
-@[alwaysInline]
+@[always_inline]
 instance : Monad (ExceptCpsT ε m) where
   map f x  := fun _ k₁ k₂ => x _ (fun a => k₁ (f a)) k₂
   pure a   := fun _ k _ => k a
@@ -39,7 +39,7 @@ instance : MonadExceptOf ε (ExceptCpsT ε m) where
   throw e  := fun _ _ k => k e
   tryCatch x handle := fun _ k₁ k₂ => x _ k₁ (fun e => handle e _ k₁ k₂)
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 def lift [Monad m] (x : m α) : ExceptCpsT ε m α :=
   fun _ k _ => x >>= k
 

src/Init/Control/Id.lean

@@ -14,7 +14,7 @@ def Id (type : Type u) : Type u := type
 
 namespace Id
 
-@[alwaysInline]
+@[always_inline]
 instance : Monad Id where
   pure x := x
   bind x f := f x
@@ -23,7 +23,7 @@ instance : Monad Id where
 def hasBind : Bind Id :=
   inferInstance
 
-@[alwaysInline, inline]
+@[always_inline, inline]
 protected def run (x : Id α) : α := x
 
 instance [OfNat α n] : OfNat (Id α) n :=