doc: docstring details (#7711)

This PR adds the last few missing docstrings that appear in the manual.

src/Init/Control/EState.lean

@@ -29,8 +29,11 @@ namespace EStateM
 
 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. -/
+/--
+Alternative orElse operator that allows callers to select which exception should be used when both
+operations fail. The default is to use the first exception since the standard `orElse` uses the
+second.
+-/
 @[always_inline, inline]
 protected def orElse' {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (useFirstEx := true) : EStateM ε σ α := fun s =>
   let d := Backtrackable.save s;
@@ -54,6 +57,11 @@ instance : MonadFinally (EStateM ε σ) := {
       | Result.error e₂ s => Result.error e₂ s
 }
 
+/--
+Converts a state monad action into a state monad action with exceptions.
+
+The resulting action does not throw an exception.
+-/
 @[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/Conv.lean

@@ -306,6 +306,10 @@ syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "| " convSe
 /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
 macro "try " t:convSeq : conv => `(conv| first | $t | skip)
 
+/--
+`tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, concatenating all goals
+produced by `tac'`.
+-/
 macro:1 x:conv tk:" <;> " y:conv:0 : conv =>
   `(conv| tactic' => (conv' => $x:conv) <;>%$tk (conv' => $y:conv))
 

src/Init/Data/String/Basic.lean

@@ -1508,12 +1508,20 @@ Checks whether the substring can be interpreted as the decimal representation of
 A substring can be interpreted as a decimal natural number if it is not empty and all the characters
 in it are digits.
 
-Use `Substring.toNat?`  to convert such a string to a natural number.
-
+Use `Substring.toNat?` to convert such a substring to a natural number.
 -/
 @[inline] def isNat (s : Substring) : Bool :=
   s.all fun c => c.isDigit
 
+/--
+Checks whether the substring can be interpreted as the decimal representation of a natural number,
+returning the number if it can.
+
+A substring can be interpreted as a decimal natural number if it is not empty and all the characters
+in it are digits.
+
+Use `Substring.isNat` to check whether the substring is such a substring.
+-/
 def toNat? (s : Substring) : Option Nat :=
   if s.isNat then
     some <| s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0

src/Init/Data/ToString/Basic.lean

@@ -11,7 +11,14 @@ open Sum Subtype Nat
 
 open Std
 
+/--
+Types that can be converted into a string for display.
+
+There is no expectation that the resulting string can be parsed back to the original data (see
+`Repr` for a similar class with this expectation).
+-/
 class ToString (α : Type u) where
+  /-- Converts a value into a string. -/
   toString : α → String
 
 export ToString (toString)

src/Init/Dynamic.lean

@@ -57,10 +57,11 @@ private opaque DynamicPointed : NonemptyType.{0} :=
   ⟨Name × NonScalar, inferInstance⟩
 
 /--
-Type-tagged union that can store any type with a `TypeName` instance.
+A type-tagged union that can store any type with a `TypeName` instance.
 
-This is roughly equivalent to `(α : Type) × TypeName α × α` but without the
-universe bump.
+This is roughly equivalent to `(α : Type) × TypeName α × α`, but without the universe bump. Use
+`Dynamic.mk` to inject a value into `Dynamic` from another type, and `Dynamic.get?` to extract a
+value from `Dynamic` if it has some expected type.
 -/
 def Dynamic : Type := DynamicPointed.type
 
@@ -92,5 +93,10 @@ opaque Dynamic.get? (α) (any : Dynamic) [TypeName α] : Option α
 private unsafe def Dynamic.mkImpl [TypeName α] (obj : α) : Dynamic :=
   unsafeCast (TypeName.typeName α, (unsafeCast obj : NonScalar))
 
+/--
+Stores the provided value in a `Dynamic`.
+
+Use `Dynamic.get? α` to retrieve it.
+-/
 @[implemented_by Dynamic.mkImpl]
 opaque Dynamic.mk [TypeName α] (obj : α) : Dynamic

src/Init/Internal/Order/Basic.lean

@@ -35,8 +35,11 @@ class PartialOrder (α : Sort u) where
   This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
   -/
   rel : α → α → Prop
+  /-- The “less-or-equal-to” or “approximates” relation is reflexive. -/
   rel_refl : ∀ {x}, rel x x
+  /-- The “less-or-equal-to” or “approximates” relation is transitive. -/
   rel_trans : ∀ {x y z}, rel x y → rel y z → rel x z
+  /-- The “less-or-equal-to” or “approximates” relation is antisymmetric. -/
   rel_antisymm : ∀ {x y}, rel x y → rel y x → x = y
 
 @[inherit_doc] scoped infix:50 " ⊑ " => PartialOrder.rel
@@ -61,15 +64,21 @@ section CCPO
 /--
 A chain-complete partial order (CCPO) is a partial order where every chain has a least upper bound.
 
-This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
+This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used
+otherwise.
 -/
 class CCPO (α : Sort u) extends PartialOrder α where
   /--
   The least upper bound of a chain.
 
-  This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
+  This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used
+  otherwise.
   -/
   csup : (α → Prop) → α
+  /--
+  `csup c` is the least upper bound of the chain `c` when all elements `x` that are at
+  least as large as `csup c` are at least as large as all elements of `c`, and vice versa.
+  -/
   csup_spec {c : α → Prop} (hc : chain c) : csup c ⊑ x ↔ (∀ y, c y → y ⊑ x)
 
 open PartialOrder CCPO

src/Init/Meta.lean

@@ -1484,12 +1484,18 @@ structure ApplyConfig where
 
 namespace Rewrite
 
+@[inherit_doc ApplyNewGoals]
 abbrev NewGoals := ApplyNewGoals
 
+/-- Configures the behavior of the `rewrite` and `rw` tactics. -/
 structure Config where
+  /-- The transparency mode to use for unfolding -/
   transparency : TransparencyMode := .reducible
+  /-- Whether to support offset constraints such as `?x + 1 =?= e` -/
   offsetCnstrs : Bool := true
+  /-- Which occurrences to rewrite-/
   occs : Occurrences := .all
+  /-- How to convert the resulting metavariables into  new goals -/
   newGoals : NewGoals := .nonDependentFirst
 
 end Rewrite

src/Init/MetaTypes.lean

@@ -20,17 +20,21 @@ structure Module where
 
 namespace Meta
 
+/--
+Which constants should be unfolded?
+-/
 inductive TransparencyMode where
-  /-- unfold all constants, even those tagged as `@[irreducible]`. -/
+  /-- Unfolds all constants, even those tagged as `@[irreducible]`. -/
   | all
-  /-- unfold all constants except those tagged as `@[irreducible]`. -/
+  /-- Unfolds all constants except those tagged as `@[irreducible]`. -/
   | default
-  /-- unfold only constants tagged with the `@[reducible]` attribute. -/
+  /-- Unfolds only constants tagged with the `@[reducible]` attribute. -/
   | reducible
-  /-- unfold reducible constants and constants tagged with the `@[instance]` attribute. -/
+  /-- Unfolds reducible constants and constants tagged with the `@[instance]` attribute. -/
   | instances
   deriving Inhabited, BEq
 
+/-- Which structure types should eta be used with? -/
 inductive EtaStructMode where
   /-- Enable eta for structure and classes. -/
   | all

src/Init/System/FilePath.lean

@@ -17,6 +17,7 @@ Paths consist of a sequence of directories followed by the name of a file or dir
 delimited by a platform-dependent separator character (see `System.FilePath.pathSeparator`).
 -/
 structure FilePath where
+  /-- The string representation of the path. -/
   toString : String
   deriving Inhabited, DecidableEq, Hashable
 

src/Init/System/IO.lean

@@ -1482,8 +1482,11 @@ The `FileRight` structure describes these permissions for a file's owner, member
 group, and all others.
 -/
 structure AccessRight where
+  /-- The file can be read. -/
   read : Bool := false
+  /-- The file can be written to. -/
   write : Bool := false
+  /-- The file can be executed. -/
   execution : Bool := false
 
 /--

src/Init/Util.lean

@@ -42,12 +42,19 @@ def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
 @[never_extract, inline] def panicWithPosWithDecl {α : Sort u} [Inhabited α] (modName : String) (declName : String) (line col : Nat) (msg : String) : α :=
   panic (mkPanicMessageWithDecl modName declName line col msg)
 
+/--
+Returns the address at which an object is allocated.
+
+This function is unsafe because it can distinguish between definitionally equal values.
+-/
 @[extern "lean_ptr_addr"]
 unsafe opaque ptrAddrUnsafe {α : Type u} (a : @& α) : USize
 
 /--
 Returns `true` if `a` is an exclusive object.
-We say an object is exclusive if it is single-threaded and its reference counter is 1.
+
+An object is exclusive if it is single-threaded and its reference counter is 1. This function is
+unsafe because it can distinguish between definitionally equal values.
 -/
 @[extern "lean_is_exclusive_obj"]
 unsafe opaque isExclusiveUnsafe {α : Type u} (a : @& α) : Bool
@@ -56,8 +63,21 @@ set_option linter.unusedVariables.funArgs false in
 @[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
   k (ptrAddrUnsafe a)
 
+/--
+Compares two objects for pointer equality.
+
+Two objects are pointer-equal if, at runtime, they are allocated at exactly the same address. This
+function is unsafe because it can distinguish between definitionally equal values.
+-/
 @[inline] unsafe def ptrEq (a b : α) : Bool := ptrAddrUnsafe a == ptrAddrUnsafe b
 
+/--
+Compares two lists of objects for element-wise pointer equality. Returns `true` if both lists are
+the same length and the objects at the corresponding indices of each list are pointer-equal.
+
+Two objects are pointer-equal if, at runtime, they are allocated at exactly the same address. This
+function is unsafe because it can distinguish between definitionally equal values.
+-/
 unsafe def ptrEqList : (as bs : List α) → Bool
   | [], [] => true
   | a::as, b::bs => if ptrEq a b then ptrEqList as bs else false

src/lake/Lake/Config/LeanConfig.lean

@@ -121,9 +121,11 @@ protected def BuildType.toString (bt : BuildType) : String :=
 
 instance : ToString BuildType := ⟨BuildType.toString⟩
 
-/-- Option that is used by Lean as if it was passed using `-D`. -/
+/-- An option that is used by Lean as if it was passed using `-D`. -/
 structure LeanOption where
+  /-- The option's name. -/
   name  : Lean.Name
+  /-- The option's value. -/
   value : Lean.LeanOptionValue
   deriving Inhabited, Repr