doc: docstring review for IntCast, NatCast, and for loops (#7645)

This PR adds missing docstrings and makes docstring style consistent for
`ForM`, `ForIn`, `ForIn'`, `ForInStep`, `IntCast`, and `NatCast`.

---------

Co-authored-by: Siddharth <siddu.druid@gmail.com>

src/Init/Control/Basic.lean

@@ -42,7 +42,9 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
   simp [binderNameHint]
   rfl -- very strange why `simp` did not close it
 
-/-- Extract the value from a `ForInStep`, ignoring whether it is `done` or `yield`. -/
+/--
+Extracts the value from a `ForInStep`, ignoring whether it is `ForInStep.done` or `ForInStep.yield`.
+-/
 def ForInStep.value (x : ForInStep α) : α :=
   match x with
   | ForInStep.done b => b
@@ -385,14 +387,20 @@ def control {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n]
   controlAt m f
 
 /--
-  Typeclass for the polymorphic `forM` operation described in the "do unchained" paper.
-  Remark:
-  - `γ` is a "container" type of elements of type `α`.
-  - `α` is treated as an output parameter by the typeclass resolution procedure.
-    That is, it tries to find an instance using only `m` and `γ`.
+Overloaded monadic iteration over some container type.
+
+An instance of `ForM m γ α` describes how to iterate a monadic operator over a container of type `γ`
+with elements of type `α` in the monad `m`. The element type should be uniquely determined by the
+monad and the container.
+
+Use `ForM.forIn` to construct a `ForIn` instance from a `ForM` instance, thus enabling the use of
+the `for` operator in `do`-notation.
 -/
 class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂)) where
-  forM [Monad m] : γ → (α → m PUnit) → m PUnit
+  /--
+  Runs the monadic action `f` on each element of the collection `coll`.
+  -/
+  forM [Monad m] (coll : γ) (f : α → m PUnit) : m PUnit
 
 export ForM (forM)
 

src/Init/Control/State.lean

@@ -159,7 +159,9 @@ instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := {
 end
 end StateT
 
-/-- Adapter to create a ForIn instance from a ForM instance -/
+/--
+Creates a suitable implementation of `ForIn.forIn` from a `ForM` instance.
+-/
 @[always_inline, inline]
 def ForM.forIn [Monad m] [ForM (StateT β (ExceptT β m)) ρ α]
     (x : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β := do

src/Init/Core.lean

@@ -294,68 +294,78 @@ inductive Exists {α : Sort u} (p : α → Prop) : Prop where
   | intro (w : α) (h : p w) : Exists p
 
 /--
-Auxiliary type used to compile `for x in xs` notation.
+An indication of whether a loop's body terminated early that's used to compile the `for x in xs`
+notation.
 
-This is the return value of the body of a `ForIn` call,
-representing the body of a for loop. It can be:
-
-* `.yield (a : α)`, meaning that we should continue the loop and `a` is the new state.
-  `.yield` is produced by `continue` and reaching the bottom of the loop body.
-* `.done (a : α)`, meaning that we should early-exit the loop with state `a`.
-  `.done` is produced by calls to `break` or `return` in the loop,
+A collection's `ForIn` or `ForIn'` instance describe's how to iterate over its elements. The monadic
+action that represents the body of the loop returns a `ForInStep α`, where `α` is the local state
+used to implement features such as `let mut`.
 -/
 inductive ForInStep (α : Type u) where
-  /-- `.done a` means that we should early-exit the loop.
-  `.done` is produced by calls to `break` or `return` in the loop. -/
+  /--
+  The loop should terminate early.
+
+  `ForInStep.done` is produced by uses of `break` or `return` in the loop body.
+  -/
   | done  : α → ForInStep α
-  /-- `.yield a` means that we should continue the loop.
-  `.yield` is produced by `continue` and reaching the bottom of the loop body. -/
+  /--
+  The loop should continue with the next iteration, using the returned state.
+
+  `ForInStep.yield` is produced by `continue` and by reaching the bottom of the loop body.
+  -/
   | yield : α → ForInStep α
   deriving Inhabited
 
 /--
-`ForIn m ρ α` is the typeclass which supports `for x in xs` notation.
-Here `xs : ρ` is the type of the collection to iterate over, `x : α`
-is the element type which is made available inside the loop, and `m` is the monad
-for the encompassing `do` block.
+Monadic iteration in `do`-blocks, using the `for x in xs` notation.
+
+The parameter `m` is the monad of the `do`-block in which iteration is performed, `ρ` is the type of
+the collection being iterated over, and `α` is the type of elements.
 -/
 class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) where
-  /-- `forIn x b f : m β` runs a for-loop in the monad `m` with additional state `β`.
-  This traverses over the "contents" of `x`, and passes the elements `a : α` to
-  `f : α → β → m (ForInStep β)`. `b : β` is the initial state, and the return value
-  of `f` is the new state as well as a directive `.done` or `.yield`
-  which indicates whether to abort early or continue iteration.
+  /--
+  Monadically iterates over the contents of a collection `xs`, with a local state `b` and the
+  possibility of early termination.
 
-  The expression
-  ```
-  let mut b := ...
-  for x in xs do
-    b ← foo x b
-  ```
-  in a `do` block is syntactic sugar for:
-  ```
-  let b := ...
-  let b ← forIn xs b (fun x b => do
-    let b ← foo x b
-    return .yield b)
-  ```
-  (Here `b` corresponds to the variables mutated in the loop.) -/
-  forIn {β} [Monad m] (x : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β
+  Because a `do` block supports local mutable bindings along with `return`, and `break`, the monadic
+  action passed to `ForIn.forIn` takes a starting state in addition to the current element of the
+  collection and returns an updated state together with an indication of whether iteration should
+  continue or terminate. If the action returns `ForInStep.done`, then `ForIn.forIn` should stop
+  iteration and return the updated state. If the action returns `ForInStep.yield`, then
+  `ForIn.forIn` should continue iterating if there are further elements, passing the updated state
+  to the action.
+
+  More information about the translation of `for` loops into `ForIn.forIn` is available in [the Lean
+  reference manual](lean-manual://section/monad-iteration-syntax).
+  -/
+  forIn {β} [Monad m] (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β
 
 export ForIn (forIn)
 
 /--
-`ForIn' m ρ α d` is a variation on the `ForIn m ρ α` typeclass which supports the
-`for h : x in xs` notation. It is the same as `for x in xs` except that `h : x ∈ xs`
-is provided as an additional argument to the body of the for-loop.
+Monadic iteration in `do`-blocks with a membership proof, using the `for h : x in xs` notation.
+
+The parameter `m` is the monad of the `do`-block in which iteration is performed, `ρ` is the type of
+the collection being iterated over, `α` is the type of elements, and `d` is the specific membership
+predicate to provide.
 -/
-class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) (d : outParam $ Membership α ρ) where
-  /-- `forIn' x b f : m β` runs a for-loop in the monad `m` with additional state `β`.
-  This traverses over the "contents" of `x`, and passes the elements `a : α` along
-  with a proof that `a ∈ x` to `f : (a : α) → a ∈ x → β → m (ForInStep β)`.
-  `b : β` is the initial state, and the return value
-  of `f` is the new state as well as a directive `.done` or `.yield`
-  which indicates whether to abort early or continue iteration. -/
+class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) (d : outParam (Membership α ρ)) where
+  /--
+  Monadically iterates over the contents of a collection `xs`, with a local state `b` and the
+  possibility of early termination. At each iteration, the body of the loop is provided with a proof
+  that the current element is in the collection.
+
+  Because a `do` block supports local mutable bindings along with `return`, and `break`, the monadic
+  action passed to `ForIn'.forIn'` takes a starting state in addition to the current element of the
+  collection with its membership proof. The action returns an updated state together with an
+  indication of whether iteration should continue or terminate. If the action returns
+  `ForInStep.done`, then `ForIn'.forIn'` should stop iteration and return the updated state. If the
+  action returns `ForInStep.yield`, then `ForIn'.forIn'` should continue iterating if there are
+  further elements, passing the updated state to the action.
+
+  More information about the translation of `for` loops into `ForIn'.forIn'` is available in [the
+  Lean reference manual](lean-manual://section/monad-iteration-syntax).
+  -/
   forIn' {β} [Monad m] (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β
 
 export ForIn' (forIn')

src/Init/Data/Cast.lean

@@ -44,25 +44,26 @@ Nat → Nat → ...`. Sometimes we also need to declare the `CoeHTCT`
 instance if we need to shadow another coercion.
 -/
 
-/-- Type class for the canonical homomorphism `Nat → R`. -/
+/--
+The canonical homomorphism `Nat → R`. In most use cases, the target type will have a (semi)ring
+structure, and this homomorphism should be a (semi)ring homomorphism.
+
+`NatCast` and `IntCast` exist to allow different libraries with their own types that can be notated
+as natural numbers to have consistent `simp` normal forms without needing to create coercion
+simplification sets that are aware of all combinations. Libraries should make it easy to work with
+`NatCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus a
+`NatCast R` instance) whenever `R` is an additive monoid with a `1`.
+
+The prototypical example is `Int.ofNat`.
+-/
 class NatCast (R : Type u) where
   /-- The canonical map `Nat → R`. -/
   protected natCast : Nat → R
 
 instance : NatCast Nat where natCast n := n
 
-/--
-Canonical homomorphism from `Nat` to a type `R`.
-
-It contains just the function, with no axioms.
-In practice, the target type will likely have a (semi)ring structure,
-and this homomorphism should be a ring homomorphism.
-
-The prototypical example is `Int.ofNat`.
-
-This class and `IntCast` exist to allow different libraries with their own types that can be notated as natural numbers to have consistent `simp` normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with `NatCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus a `NatCast R` instance) whenever `R` is an additive monoid with a `1`.
--/
-@[coe, reducible, match_pattern] protected def Nat.cast {R : Type u} [NatCast R] : Nat → R :=
+@[coe, reducible, match_pattern, inherit_doc NatCast]
+protected def Nat.cast {R : Type u} [NatCast R] : Nat → R :=
   NatCast.natCast
 
 -- see the notes about coercions into arbitrary types in the module doc-string

src/Init/Data/Int/Basic.lean

@@ -401,8 +401,14 @@ instance : Max Int := maxOfLe
 end Int
 
 /--
-The canonical homomorphism `Int → R`.
-In most use cases `R` will have a ring structure and this will be a ring homomorphism.
+The canonical homomorphism `Int → R`. In most use cases, the target type will have a ring structure,
+and this homomorphism should be a ring homomorphism.
+
+`IntCast` and `NatCast` exist to allow different libraries with their own types that can be notated
+as natural numbers to have consistent `simp` normal forms without needing to create coercion
+simplification sets that are aware of all combinations. Libraries should make it easy to work with
+`IntCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus an
+`IntCast R` instance) whenever `R` is an additive group with a `1`.
 -/
 class IntCast (R : Type u) where
   /-- The canonical map `Int → R`. -/
@@ -410,12 +416,8 @@ class IntCast (R : Type u) where
 
 instance : IntCast Int where intCast n := n
 
-/--
-Apply the canonical homomorphism from `Int` to a type `R` from an `IntCast R` instance.
-
-In Mathlib there will be such a homomorphism whenever `R` is an additive group with a `1`.
--/
-@[coe, reducible, match_pattern] protected def Int.cast {R : Type u} [IntCast R] : Int → R :=
+@[coe, reducible, match_pattern, inherit_doc IntCast]
+protected def Int.cast {R : Type u} [IntCast R] : Int → R :=
   IntCast.intCast
 
 -- see the notes about coercions into arbitrary types in the module doc-string

src/Init/System/IO.lean

@@ -439,7 +439,17 @@ may throw an exception of type `IO.Error`, the result of the task is an `Except
     (prio := Task.Priority.default) (sync := false) : BaseIO (Task (Except IO.Error β)) :=
   EIO.bindTask t f prio sync
 
-/-- `IO` specialization of `EIO.chainTask`. -/
+/--
+Creates a new task that waits for `t` to complete and then runs the `IO` action `f` on its result.
+This new task has priority `prio`.
+
+This is a version of `IO.mapTask` that ignores the result value.
+
+Running the resulting `IO` action causes the task to be started eagerly. Unlike pure tasks created
+by `Task.spawn`, tasks created by this function will run even if the last reference to the task is
+dropped. The act should explicitly check for cancellation via `IO.checkCanceled` if it should be
+terminated or otherwise react to the last reference being dropped.
+-/
 def chainTask (t : Task α) (f : α → IO Unit) (prio := Task.Priority.default)
     (sync := false) : IO Unit :=
   EIO.chainTask t f prio sync