[Merged by Bors] - chore(Lean,Tactic): un-indent some doc-strings

Mathlib/Lean/Expr/Basic.lean

@@ -45,9 +45,9 @@ def mapPrefix (f : Name → Option Name) (n : Name) : Name := Id.run do
   | str n' s => mkStr (mapPrefix f n') s
   | num n' i => mkNum (mapPrefix f n') i
 
-/-- Build a name from components. For example ``from_components [`foo, `bar]`` becomes
-  ``` `foo.bar```.
-  It is the inverse of `Name.components` on list of names that have single components. -/
+/-- Build a name from components.
+For example, ``from_components [`foo, `bar]`` becomes ``` `foo.bar```.
+It is the inverse of `Name.components` on list of names that have single components. -/
 def fromComponents : List Name → Name := go .anonymous where
   /-- Auxiliary for `Name.fromComponents` -/
   go : Name → List Name → Name
@@ -66,16 +66,16 @@ def lastComponentAsString : Name → String
   | .num _ n => toString n
   | .anonymous => ""
 
-/-- `nm.splitAt n` splits a name `nm` in two parts, such that the *second* part has depth `n`, i.e.
-  `(nm.splitAt n).2.getNumParts = n` (assuming `nm.getNumParts ≥ n`).
-  Example: ``splitAt `foo.bar.baz.back.bat 1 = (`foo.bar.baz.back, `bat)``. -/
+/-- `nm.splitAt n` splits a name `nm` in two parts, such that the *second* part has depth `n`,
+i.e. `(nm.splitAt n).2.getNumParts = n` (assuming `nm.getNumParts ≥ n`).
+Example: ``splitAt `foo.bar.baz.back.bat 1 = (`foo.bar.baz.back, `bat)``. -/
 def splitAt (nm : Name) (n : Nat) : Name × Name :=
   let (nm2, nm1) := nm.componentsRev.splitAt n
   (.fromComponents <| nm1.reverse, .fromComponents <| nm2.reverse)
 
 /-- `isPrefixOf? pre nm` returns `some post` if `nm = pre ++ post`.
-  Note that this includes the case where `nm` has multiple more namespaces.
-  If `pre` is not a prefix of `nm`, it returns `none`. -/
+Note that this includes the case where `nm` has multiple more namespaces.
+If `pre` is not a prefix of `nm`, it returns `none`. -/
 def isPrefixOf? (pre nm : Name) : Option Name :=
   if pre == nm then
     some anonymous
@@ -212,8 +212,8 @@ def type? : Expr → Option Level
   | _ => none
 
 /-- `isConstantApplication e` checks whether `e` is syntactically an application of the form
-  `(fun x₁ ⋯ xₙ => H) y₁ ⋯ yₙ` where `H` does not contain the variable `xₙ`. In other words,
-  it does a syntactic check that the expression does not depend on `yₙ`. -/
+`(fun x₁ ⋯ xₙ => H) y₁ ⋯ yₙ` where `H` does not contain the variable `xₙ`. In other words,
+it does a syntactic check that the expression does not depend on `yₙ`. -/
 def isConstantApplication (e : Expr) :=
   e.isApp && aux e.getAppNumArgs'.pred e.getAppFn' e.getAppNumArgs'
 where
@@ -252,11 +252,11 @@ def ofInt (α : Expr) : Int → MetaM Expr
 section recognizers
 
 /--
-  Return `some n` if `e` is one of the following
-  - A nat literal (numeral)
-  - `Nat.zero`
-  - `Nat.succ x` where `isNumeral x`
-  - `OfNat.ofNat _ x _` where `isNumeral x` -/
+Return `some n` if `e` is one of the following
+- a nat literal (numeral)
+- `Nat.zero`
+- `Nat.succ x` where `isNumeral x`
+- `OfNat.ofNat _ x _` where `isNumeral x` -/
 partial def numeral? (e : Expr) : Option Nat :=
   if let some n := e.rawNatLit? then n
   else
@@ -450,9 +450,9 @@ def rewriteType (e eq : Expr) : MetaM Expr := do
   mkEqMP (← (← inferType e).rewrite eq) e
 
 /-- Given `(hNotEx : Not ex)` where `ex` is of the form `Exists x, p x`,
-    return a `forall x, Not (p x)` and a proof for it.
+return a `forall x, Not (p x)` and a proof for it.
 
-    This function handles nested existentials. -/
+This function handles nested existentials. -/
 partial def forallNot_of_notExists (ex hNotEx : Expr) : MetaM (Expr × Expr) := do
   let .app (.app (.const ``Exists [lvl]) A) p := ex | failure
   go lvl A p hNotEx
@@ -482,7 +482,7 @@ where
 end Expr
 
 /-- Get the projections that are projections to parent structures. Similar to `getParentStructures`,
-  except that this returns the (last component of the) projection names instead of the parent names.
+except that this returns the (last component of the) projection names instead of the parent names.
 -/
 def getFieldsToParents (env : Environment) (structName : Name) : Array Name :=
   getStructureFields env structName |>.filter fun fieldName =>

Mathlib/Lean/Meta/Simp.lean

@@ -126,7 +126,7 @@ def isInSimpSet (simpAttr decl : Name) : CoreM Bool := do
   return (← simpDecl.getTheorems).contains decl
 
 /-- Returns all declarations with the `simp`-attribute `simpAttr`.
-  Note: this also returns many auxiliary declarations. -/
+Note: this also returns many auxiliary declarations. -/
 def getAllSimpDecls (simpAttr : Name) : CoreM (List Name) := do
   let .some simpDecl ← getSimpExtension? simpAttr | return []
   let thms ← simpDecl.getTheorems

Mathlib/Logic/IsEmpty.lean

@@ -106,7 +106,7 @@ protected def elim {α : Sort u} (_ : IsEmpty α) {p : α → Sort*} (a : α) :
   isEmptyElim a
 
 /-- Non-dependent version of `IsEmpty.elim`. Helpful if the elaborator cannot elaborate `h.elim a`
-  correctly. -/
+correctly. -/
 protected def elim' {β : Sort*} (h : IsEmpty α) (a : α) : β :=
   (h.false a).elim
 

Mathlib/Logic/Nonempty.lean

@@ -68,9 +68,8 @@ theorem nonempty_plift {α} : Nonempty (PLift α) ↔ Nonempty α :=
   Iff.intro (fun ⟨⟨a⟩⟩ ↦ ⟨a⟩) fun ⟨a⟩ ↦ ⟨⟨a⟩⟩
 
 /-- Using `Classical.choice`, lifts a (`Prop`-valued) `Nonempty` instance to a (`Type`-valued)
-  `Inhabited` instance. `Classical.inhabited_of_nonempty` already exists, in
-  `Init/Classical.lean`, but the assumption is not a type class argument,
-  which makes it unsuitable for some applications. -/
+`Inhabited` instance. `Classical.inhabited_of_nonempty` already exists, in `Init/Classical.lean`,
+but the assumption is not a type class argument, which makes it unsuitable for some applications. -/
 noncomputable def Classical.inhabited_of_nonempty' {α} [h : Nonempty α] : Inhabited α :=
   ⟨Classical.choice h⟩
 
@@ -83,7 +82,7 @@ protected noncomputable abbrev Classical.arbitrary (α) [h : Nonempty α] : α :
   Classical.choice h
 
 /-- Given `f : α → β`, if `α` is nonempty then `β` is also nonempty.
-  `Nonempty` cannot be a `functor`, because `Functor` is restricted to `Type`. -/
+`Nonempty` cannot be a `functor`, because `Functor` is restricted to `Type`. -/
 theorem Nonempty.map {α β} (f : α → β) : Nonempty α → Nonempty β
   | ⟨h⟩ => ⟨f h⟩
 

Mathlib/Tactic/Core.lean

@@ -190,8 +190,8 @@ def allGoals (tac : TacticM Unit) : TacticM Unit := do
           throw ex
   setGoals mvarIdsNew.toList
 
-/-- Simulates the `<;>` tactic combinator. First runs `tac1` and then runs
-    `tac2` on all newly-generated subgoals.
+/-- Simulates the `<;>` tactic combinator.
+First runs `tac1` and then runs `tac2` on all newly-generated subgoals.
 -/
 def andThenOnSubgoals (tac1 : TacticM Unit) (tac2 : TacticM Unit) : TacticM Unit :=
   focus do tac1; allGoals tac2

Mathlib/Tactic/Inhabit.lean

@@ -32,7 +32,7 @@ If the target is a `Prop`, this is done constructively. Otherwise, it uses `Clas
 syntax (name := inhabit) "inhabit " atomic(ident " : ")? term : tactic
 
 /-- `evalInhabit` takes in the MVarId of the main goal, runs the core portion of the inhabit tactic,
-    and returns the resulting MVarId -/
+and returns the resulting MVarId -/
 def evalInhabit (goal : MVarId) (h_name : Option Ident) (term : Syntax) : TacticM MVarId := do
   goal.withContext do
     let e ← Tactic.elabTerm term none

Mathlib/Tactic/Simps/Basic.lean

@@ -55,8 +55,8 @@ open Meta hiding Config
 open Elab.Term hiding mkConst
 
 /-- `updateName nm s isPrefix` adds `s` to the last component of `nm`,
-  either as prefix or as suffix (specified by `isPrefix`), separated by `_`.
-  Used by `simps_add_projections`. -/
+either as prefix or as suffix (specified by `isPrefix`), separated by `_`.
+Used by `simps_add_projections`. -/
 def updateName (nm : Name) (s : String) (isPrefix : Bool) : Name :=
   nm.updateLast fun s' ↦ if isPrefix then s ++ "_" ++ s' else s' ++ "_" ++ s
 
@@ -423,7 +423,7 @@ instance : ToMessageData ParsedProjectionData where toMessageData
     ("," ++ Format.line) ++ "⟩"
 
 /-- The type of rules that specify how metadata for projections in changes.
-  See `initialize_simps_projections`. -/
+See `initialize_simps_projections`. -/
 inductive ProjectionRule where
   /-- A renaming rule `before→after` or
     Each name comes with the syntax used to write the rule,
@@ -528,19 +528,20 @@ partial def getCompositeOfProjectionsAux (proj : String) (e : Expr) (pos : Array
     getCompositeOfProjectionsAux projRest (mkAppN newE typeArgs) newPos (args ++ typeArgs)
 
 /-- Suppose we are given a structure `str` and a projection `proj`, that could be multiple nested
-  projections (separated by `_`), where each projection could be a projection of a parent structure.
-  This function returns an expression that is the composition of these projections and a
-  list of natural numbers, that are the projection numbers of the applied projections.
-  Note that this function is similar to elaborating dot notation, but it can do a little more.
-  Example: if we do
-  ```
-  structure gradedFun (A : ℕ → Type*) where
-    toFun := ∀ i j, A i →+ A j →+ A (i + j)
-  initialize_simps_projections (toFun_toFun_toFun → myMul)
-  ```
-  we will be able to generate the "projection"
-    `fun {A} (f : gradedFun A) (x : A i) (y : A j) ↦ ↑(↑(f.toFun i j) x) y`,
-  which projection notation cannot do. -/
+projections (separated by `_`), where each projection could be a projection of a parent structure.
+This function returns an expression that is the composition of these projections and a
+list of natural numbers, that are the projection numbers of the applied projections.
+Note that this function is similar to elaborating dot notation, but it can do a little more.
+
+Example: if we do
+```
+structure gradedFun (A : ℕ → Type*) where
+  toFun := ∀ i j, A i →+ A j →+ A (i + j)
+initialize_simps_projections (toFun_toFun_toFun → myMul)
+```
+we will be able to generate the "projection"
+  `fun {A} (f : gradedFun A) (x : A i) (y : A j) ↦ ↑(↑(f.toFun i j) x) y`,
+which projection notation cannot do. -/
 def getCompositeOfProjections (structName : Name) (proj : String) : MetaM (Expr × Array Nat) := do
   let strExpr ← mkConstWithLevelParams structName
   let type ← inferType strExpr
@@ -549,9 +550,9 @@ def getCompositeOfProjections (structName : Name) (proj : String) : MetaM (Expr
   getCompositeOfProjectionsAux (proj ++ "_") e #[] <| typeArgs.push e
 
 /-- Get the default `ParsedProjectionData` for structure `str`.
-  It first returns the direct fields of the structure in the right order, and then
-  all (non-subobject fields) of all parent structures. The subobject fields are precisely the
-  non-default fields. -/
+It first returns the direct fields of the structure in the right order, and then
+all (non-subobject fields) of all parent structures. The subobject fields are precisely the
+non-default fields. -/
 def mkParsedProjectionData (structName : Name) : CoreM (Array ParsedProjectionData) := do
   let env ← getEnv
   let projs := getStructureFields env structName
@@ -613,8 +614,8 @@ def applyProjectionRules (projs : Array ParsedProjectionData) (rules : Array Pro
   pure projs
 
 /-- Auxiliary function for `getRawProjections`.
-  Generates the default projection, and looks for a custom projection declared by the user,
-  and replaces the default projection with the custom one, if it can find it. -/
+Generates the default projection, and looks for a custom projection declared by the user,
+and replaces the default projection with the custom one, if it can find it. -/
 def findProjection (str : Name) (proj : ParsedProjectionData)
     (rawUnivs : List Level) : CoreM ParsedProjectionData := do
   let env ← getEnv
@@ -652,7 +653,7 @@ def findProjection (str : Name) (proj : ParsedProjectionData)
     pure {proj with expr? := some rawExpr, projNrs := nrs}
 
 /-- Checks if there are declarations in the current file in the namespace `{str}.Simps` that are
-  not used. -/
+not used. -/
 def checkForUnusedCustomProjs (stx : Syntax) (str : Name) (projs : Array ParsedProjectionData) :
     CoreM Unit := do
   let nrCustomProjections := projs.toList.countP (·.isCustom)
@@ -827,7 +828,7 @@ composite of multiple projections).
 -/
 
 /-- Parse a rule for `initialize_simps_projections`. It is `<name>→<name>`, `-<name>`, `+<name>`
-  or `as_prefix <name>`. -/
+or `as_prefix <name>`. -/
 def elabSimpsRule : Syntax → CommandElabM ProjectionRule
   | `(simpsRule| $id1 → $id2)   => return .rename id1.getId id1.raw id2.getId id2.raw
   | `(simpsRule| - $id)         => return .erase id.getId id.raw
@@ -874,12 +875,12 @@ structure Config where
 declare_command_config_elab elabSimpsConfig Config
 
 /-- A common configuration for `@[simps]`: generate equalities between functions instead equalities
-  between fully applied Expressions. Use this using `@[simps (config := .asFn)]`. -/
+between fully applied Expressions. Use this using `@[simps (config := .asFn)]`. -/
 def Config.asFn : Simps.Config where
   fullyApplied := false
 
 /-- A common configuration for `@[simps]`: don't tag the generated lemmas with `@[simp]`.
-  Use this using `@[simps (config := .lemmasOnly)]`. -/
+Use this using `@[simps (config := .lemmasOnly)]`. -/
 def Config.lemmasOnly : Config where
   isSimp := false
 
@@ -893,14 +894,14 @@ partial def _root_.Lean.Expr.instantiateLambdasOrApps (es : Array Expr) (e : Exp
   e.betaRev es.reverse true -- check if this is what I want
 
 /-- Get the projections of a structure used by `@[simps]` applied to the appropriate arguments.
-  Returns a list of tuples
-  ```
-  (corresponding right-hand-side, given projection name, projection Expression,
-    future projection numbers, used by default, is prefix)
-  ```
-  (where all fields except the first are packed in a `ProjectionData` structure)
-  one for each projection. The given projection name is the name for the projection used by the user
-  used to generate (and parse) projection names. For example, in the structure
+Returns a list of tuples
+```
+(corresponding right-hand-side, given projection name, projection Expression,
+  future projection numbers, used by default, is prefix)
+```
+(where all fields except the first are packed in a `ProjectionData` structure)
+one for each projection. The given projection name is the name for the projection used by the user
+used to generate (and parse) projection names. For example, in the structure
 
   Example 1: ``getProjectionExprs env `(α × β) `(⟨x, y⟩)`` will give the output
   ```
@@ -941,7 +942,7 @@ def getProjectionExprs (stx : Syntax) (tgt : Expr) (rhs : Expr) (cfg : Config) :
 variable (ref : Syntax) (univs : List Name)
 
 /-- Add a lemma with `nm` stating that `lhs = rhs`. `type` is the type of both `lhs` and `rhs`,
-  `args` is the list of local constants occurring, and `univs` is the list of universe variables. -/
+`args` is the list of local constants occurring, and `univs` is the list of universe variables. -/
 def addProjection (declName : Name) (type lhs rhs : Expr) (args : Array Expr)
     (cfg : Config) : MetaM Unit := do
   trace[simps.debug] "Planning to add the equality{indentD m!"{lhs} = ({rhs} : {type})"}"
@@ -1169,9 +1170,9 @@ end Simps
 open Simps
 
 /-- `simpsTac` derives `simp` lemmas for all (nested) non-Prop projections of the declaration.
-  If `todo` is non-empty, it will generate exactly the names in `todo`.
-  If `shortNm` is true, the generated names will only use the last projection name.
-  If `trc` is true, trace as if `trace.simps.verbose` is true. -/
+If `todo` is non-empty, it will generate exactly the names in `todo`.
+If `shortNm` is true, the generated names will only use the last projection name.
+If `trc` is true, trace as if `trace.simps.verbose` is true. -/
 def simpsTac (ref : Syntax) (nm : Name) (cfg : Config := {})
     (todo : List (String × Syntax) := []) (trc := false) : AttrM (Array Name) :=
   withOptions (· |>.updateBool `trace.simps.verbose (trc || ·)) <| do

Mathlib/Tactic/Simps/NotationClass.lean

@@ -20,7 +20,7 @@ in the file where we declare `@[simps]`. For further documentation, see `Tactic.
 -/
 
 /-- The `@[notation_class]` attribute specifies that this is a notation class,
-  and this notation should be used instead of projections by `@[simps]`.
+and this notation should be used instead of projections by `@[simps]`.
   * This is only important if the projection is written differently using notation, e.g.
     `+` uses `HAdd.hAdd`, not `Add.add` and `0` uses `OfNat.ofNat` not `Zero.zero`.
     We also add it to non-heterogenous notation classes, like `Neg`, but it doesn't do much for any
@@ -87,7 +87,7 @@ def findCoercionArgs : findArgType := fun str className args ↦ do
   return #[some eStr] ++ classArgs
 
 /-- Data needed to generate automatic projections. This data is associated to a name of a projection
-  in a structure that must be used to trigger the search. -/
+in a structure that must be used to trigger the search. -/
 structure AutomaticProjectionData where
   /-- `className` is the name of the class we are looking for. -/
   className : Name
@@ -100,7 +100,7 @@ structure AutomaticProjectionData where
 deriving Inhabited
 
 /-- `@[notation_class]` attribute. Note: this is *not* a `NameMapAttribute` because we key on the
-  argument of the attribute, not the declaration name. -/
+argument of the attribute, not the declaration name. -/
 initialize notationClassAttr : NameMapExtension AutomaticProjectionData ← do
   let ext ← registerNameMapExtension AutomaticProjectionData
   registerBuiltinAttribute {