chore(*): replace uses of --- delimiter in tactic docs (#2372)

* update abel doc string

the tactic doc entry seems completely fine as the doc string,
I don't know why these were separated

* replace uses of --- in docs

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/tactic/abel.lean

@@ -319,14 +319,7 @@ do mode ← ident?, match mode with
 | _          := failed
 end
 
-/-- Tactic for solving equations in the language of
-*additive*, commutative monoids and groups.
-Attempts to prove the goal outright if there is no `at`
-specifier and the target is an equality, but if this
-fails it falls back to rewriting all monoid expressions
-into a normal form.
-
----
+/--
 Evaluate expressions in the language of *additive*, commutative monoids and groups.
 It attempts to prove the goal outright if there is no `at`
 specifier and the target is an equality, but if this

src/tactic/clear.lean

@@ -65,9 +65,21 @@ In contrast to `clear`, the order of hypotheses
 does not matter, even if there are dependencies between them. Fails if the
 target or any local hypotheses (other than the given ones) depend on the given
 hypotheses.
+-/
+meta def clear' (p : parse (many ident)) : tactic unit := do
+hyps ← p.mmap get_local,
+tactic.clear' false (rb_map.set_of_list hyps)
 
----
+/-- `clear_dependent a b c` removes from the local context
+the given hypotheses and any other hypotheses that depend on them.
+The hypotheses can be given in any order. Fails if the target depends on any of
+the given hypotheses.
+ -/
+meta def clear_dependent (p : parse (many ident)) : tactic unit := do
+hyps ← p.mmap get_local,
+tactic.clear' true (rb_map.set_of_list hyps)
 
+/--
 An improved version of the standard `clear` tactic. `clear` is sensitive to the
 order of its arguments: `clear x y` may fail even though both `x` and `y` could
 be cleared (if the type of `y` depends on `x`). `clear'` lifts this limitation.
@@ -81,17 +93,14 @@ begin
 end
 ```
 -/
-meta def clear' (p : parse (many ident)) : tactic unit := do
-hyps ← p.mmap get_local,
-tactic.clear' false (rb_map.set_of_list hyps)
-
-/-- `clear_dependent a b c` removes from the local context
-the given hypotheses and any other hypotheses that depend on them.
-The hypotheses can be given in any order. Fails if the target depends on any of
-the given hypotheses.
-
----
+add_tactic_doc
+{ name       := "clear'",
+  category   := doc_category.tactic,
+  decl_names := [`tactic.interactive.clear', `tactic.interactive.clear_dependent],
+  tags       := ["context management"],
+  inherit_description_from := `tactic.interactive.clear' }
 
+/--
 A variant of `clear'` which clears not only the given hypotheses, but also any
 other hypotheses depending on them.
 
@@ -103,18 +112,7 @@ begin
   exact ()
 end
 ```
- -/
-meta def clear_dependent (p : parse (many ident)) : tactic unit := do
-hyps ← p.mmap get_local,
-tactic.clear' true (rb_map.set_of_list hyps)
-
-add_tactic_doc
-{ name       := "clear'",
-  category   := doc_category.tactic,
-  decl_names := [`tactic.interactive.clear', `tactic.interactive.clear_dependent],
-  tags       := ["context management"],
-  inherit_description_from := `tactic.interactive.clear' }
-
+-/
 add_tactic_doc
 { name       := "clear_dependent",
   category   := doc_category.tactic,

src/tactic/doc_commands.lean

@@ -80,49 +80,6 @@ note message
 -/
 library_note "note id"
 ```
-
----
-
-At various places in mathlib, we leave implementation notes that are referenced from many other
-files. To keep track of these notes, we use the command `library_note`. This makes it easy to
-retrieve a list of all notes, e.g. for documentation output.
-
-These notes can be referenced in mathlib with the syntax `Note [note id]`.
-Often, these references will be made in code comments (`--`) that won't be displayed in docs.
-If such a reference is made in a doc string or module doc, it will be linked to the corresponding
-note in the doc display.
-
-Syntax:
-```
-/--
-note message
--/
-library_note "note id"
-```
-
-An example from `meta.expr`:
-
-```
-/--
-Some declarations work with open expressions, i.e. an expr that has free variables.
-Terms will free variables are not well-typed, and one should not use them in tactics like
-`infer_type` or `unify`. You can still do syntactic analysis/manipulation on them.
-The reason for working with open types is for performance: instantiating variables requires
-iterating through the expression. In one performance test `pi_binders` was more than 6x
-quicker than `mk_local_pis` (when applied to the type of all imported declarations 100x).
--/
-library_note "open expressions"
-```
-
-This note can be referenced near a usage of `pi_binders`:
-
-
-```
--- See Note [open expressions]
-/-- behavior of f -/
-def f := pi_binders ...
-```
-
 -/
 @[user_command] meta def library_note (mi : interactive.decl_meta_info)
   (_ : parse (tk "library_note")) : parser unit := do
@@ -274,6 +231,47 @@ let e : tactic_doc_entry := match mi.doc_string with
   end,
 tactic.add_tactic_doc e .
 
+/--
+At various places in mathlib, we leave implementation notes that are referenced from many other
+files. To keep track of these notes, we use the command `library_note`. This makes it easy to
+retrieve a list of all notes, e.g. for documentation output.
+
+These notes can be referenced in mathlib with the syntax `Note [note id]`.
+Often, these references will be made in code comments (`--`) that won't be displayed in docs.
+If such a reference is made in a doc string or module doc, it will be linked to the corresponding
+note in the doc display.
+
+Syntax:
+```
+/--
+note message
+-/
+library_note "note id"
+```
+
+An example from `meta.expr`:
+
+```
+/--
+Some declarations work with open expressions, i.e. an expr that has free variables.
+Terms will free variables are not well-typed, and one should not use them in tactics like
+`infer_type` or `unify`. You can still do syntactic analysis/manipulation on them.
+The reason for working with open types is for performance: instantiating variables requires
+iterating through the expression. In one performance test `pi_binders` was more than 6x
+quicker than `mk_local_pis` (when applied to the type of all imported declarations 100x).
+-/
+library_note "open expressions"
+```
+
+This note can be referenced near a usage of `pi_binders`:
+
+
+```
+-- See Note [open expressions]
+/-- behavior of f -/
+def f := pi_binders ...
+```
+-/
 add_tactic_doc
 { name                     := "library_note",
   category                 := doc_category.cmd,

src/tactic/hint.lean

@@ -73,9 +73,18 @@ do names ← attribute.get_instances `hint_tactic,
 
 namespace interactive
 
-/-- report a list of tactics that can make progress against the current goal
+/--
+report a list of tactics that can make progress against the current goal
+-/
+meta def hint : tactic unit :=
+do hints ← tactic.hint,
+   if hints.length = 0 then
+     fail "no hints available"
+   else
+     do trace "the following tactics make progress:\n----",
+        hints.mmap' (λ s, tactic.trace format!"Try this: {s}")
 
----
+/--
 `hint` lists possible tactics which will make progress (that is, not fail) against the current goal.
 
 ```lean
@@ -98,14 +107,6 @@ You can add a tactic to the list that `hint` tries by either using
 tactic), or
 2. `add_hint_tactic "my_tactic"`, specifying a string which works as an interactive tactic.
 -/
-meta def hint : tactic unit :=
-do hints ← tactic.hint,
-   if hints.length = 0 then
-     fail "no hints available"
-   else
-     do trace "the following tactics make progress:\n----",
-        hints.mmap' (λ s, tactic.trace format!"Try this: {s}")
-
 add_tactic_doc
 { name        := "hint",
   category    := doc_category.tactic,

src/tactic/interval_cases.lean

@@ -219,8 +219,39 @@ You can also explicitly specify a lower and upper bound to use,
 as `interval_cases using hl hu`.
 The hypotheses should be in the form `hl : a ≤ n` and `hu : n < b`,
 in which case `interval_cases` calls `fin_cases` on the resulting fact `n ∈ set.Ico a b`.
+-/
+meta def interval_cases (n : parse texpr?) (bounds : parse (tk "using" *> (prod.mk <$> ident <*> ident))?) : tactic unit :=
+do
+  if h : n.is_some then (do
+    guard bounds.is_none <|> fail "Do not use the `using` keyword if specifying the variable explicitly.",
+    n ← to_expr (option.get h),
+    (hl, hu) ← get_bounds n,
+    tactic.interval_cases_using hl hu)
+  else if h' : bounds.is_some then (do
+    [hl, hu] ← [(option.get h').1, (option.get h').2].mmap get_local,
+    tactic.interval_cases_using hl hu)
+  else
+    fail "Call `interval_cases n` (specifying a variable), or `interval_cases lb ub` (specifying a lower bound and upper bound on the same variable)."
 
----
+/--
+`interval_cases n` searches for upper and lower bounds on a variable `n`,
+and if bounds are found,
+splits into separate cases for each possible value of `n`.
+
+As an example, in
+```
+example (n : ℕ) (w₁ : n ≥ 3) (w₂ : n < 5) : n = 3 ∨ n = 4 :=
+begin
+  interval_cases n,
+  all_goals {simp}
+end
+```
+after `interval_cases n`, the goals are `3 = 3 ∨ 3 = 4` and `4 = 3 ∨ 4 = 4`.
+
+You can also explicitly specify a lower and upper bound to use,
+as `interval_cases using hl hu`.
+The hypotheses should be in the form `hl : a ≤ n` and `hu : n < b`,
+in which case `interval_cases` calls `fin_cases` on the resulting fact `n ∈ set.Ico a b`.
 
 In particular, `interval_cases n`
 1) inspects hypotheses looking for lower and upper bounds of the form `a ≤ n` and `n < b`
@@ -238,19 +269,6 @@ The variable `n` can belong to any type `α`, with the following restrictions:
 * if multiple bounds are located, an instance of `decidable_linear_order α` is available, and
 * an instance of `fintype set.Ico l u` is available for the relevant bounds.
 -/
-meta def interval_cases (n : parse texpr?) (bounds : parse (tk "using" *> (prod.mk <$> ident <*> ident))?) : tactic unit :=
-do
-  if h : n.is_some then (do
-    guard bounds.is_none <|> fail "Do not use the `using` keyword if specifying the variable explicitly.",
-    n ← to_expr (option.get h),
-    (hl, hu) ← get_bounds n,
-    tactic.interval_cases_using hl hu)
-  else if h' : bounds.is_some then (do
-    [hl, hu] ← [(option.get h').1, (option.get h').2].mmap get_local,
-    tactic.interval_cases_using hl hu)
-  else
-    fail "Call `interval_cases n` (specifying a variable), or `interval_cases lb ub` (specifying a lower bound and upper bound on the same variable)."
-
 add_tactic_doc
 { name       := "interval_cases",
   category   := doc_category.tactic,

src/tactic/linarith.lean

@@ -830,9 +830,25 @@ Config options:
 * `linarith {restrict_type := T}` will run only on hypotheses that are inequalities over `T`
 * `linarith {discharger := tac}` will use `tac` instead of `ring` for normalization.
   Options: `ring2`, `ring SOP`, `simp`
+-/
+meta def tactic.interactive.linarith (red : parse ((tk "!")?))
+  (restr : parse ((tk "only")?)) (hyps : parse pexpr_list?)
+  (cfg : linarith_config := {}) : tactic unit :=
+let cfg :=
+  if red.is_some then {cfg with transparency := semireducible, discharger := `[ring!]}
+  else cfg in
+do t ← target,
+   when cfg.split_hypotheses (try auto.split_hyps),
+   match get_contr_lemma_name t with
+   | some nm := seq (applyc nm) $
+     do t ← intro1, linarith.interactive_aux cfg (some t) restr.is_some hyps
+   | none := if cfg.exfalso then exfalso >> linarith.interactive_aux cfg none restr.is_some hyps
+             else fail "linarith failed: target type is not an inequality."
+   end
 
----
+add_hint_tactic "linarith"
 
+/--
 `linarith` attempts to find a contradiction between hypotheses that are linear (in)equalities.
 Equivalently, it can prove a linear inequality by assuming its negation and proving `false`.
 
@@ -876,25 +892,7 @@ optional arguments:
   hypotheses.
 * If `exfalso` is false, `linarith` will fail when the goal is neither an inequality nor `false`.
   (True by default.)
-
 -/
-meta def tactic.interactive.linarith (red : parse ((tk "!")?))
-  (restr : parse ((tk "only")?)) (hyps : parse pexpr_list?)
-  (cfg : linarith_config := {}) : tactic unit :=
-let cfg :=
-  if red.is_some then {cfg with transparency := semireducible, discharger := `[ring!]}
-  else cfg in
-do t ← target,
-   when cfg.split_hypotheses (try auto.split_hyps),
-   match get_contr_lemma_name t with
-   | some nm := seq (applyc nm) $
-     do t ← intro1, linarith.interactive_aux cfg (some t) restr.is_some hyps
-   | none := if cfg.exfalso then exfalso >> linarith.interactive_aux cfg none restr.is_some hyps
-             else fail "linarith failed: target type is not an inequality."
-   end
-
-add_hint_tactic "linarith"
-
 add_tactic_doc
 { name       := "linarith",
   category   := doc_category.tactic,

src/tactic/omega/main.lean

@@ -83,9 +83,17 @@ Guesses the correct domain by looking at the goal and hypotheses,
 and then reverts all relevant hypotheses and variables.
 Use `omega manual` to disable automatic reverts, and `omega int` or
 `omega nat` to specify the domain.
+-/
+meta def tactic.interactive.omega (opt : parse (many ident)) : tactic unit :=
+do is_int ← determine_domain opt,
+   let is_manual : bool := if `manual ∈ opt then tt else ff,
+   if is_int
+   then omega_int is_manual
+   else omega_nat is_manual
 
----
+add_hint_tactic "omega"
 
+/--
 `omega` attempts to discharge goals in the quantifier-free fragment of linear integer and natural number arithmetic using the Omega test. In other words, the core procedure of `omega` works with goals of the form
 ```lean
 ∀ x₁, ... ∀ xₖ, P
@@ -112,15 +120,6 @@ by {revert h2 i, omega manual int}
 
 `omega` implements the real shadow step of the Omega test, but not the dark and gray shadows. Therefore, it should (in principle) succeed whenever the negation of the goal has no real solution, but it may fail if a real solution exists, even if there is no integer/natural number solution.
 -/
-meta def tactic.interactive.omega (opt : parse (many ident)) : tactic unit :=
-do is_int ← determine_domain opt,
-   let is_manual : bool := if `manual ∈ opt then tt else ff,
-   if is_int
-   then omega_int is_manual
-   else omega_nat is_manual
-
-add_hint_tactic "omega"
-
 add_tactic_doc
 { name       := "omega",
   category   := doc_category.tactic,

src/tactic/reassoc_axiom.lean

@@ -215,8 +215,11 @@ begin
   rw [h',reassoc_of h],
 end
 ```
----
+-/
+theorem category_theory.reassoc_of {α} (hh : α) {β}
+  (x : tactic.calculated_Prop β hh . tactic.derive_reassoc_proof) : β := x
 
+/--
 `reassoc_of h` takes local assumption `h` and add a ` ≫ f` term on the right of
 both sides of the equality. Instead of creating a new assumption from the result, `reassoc_of h`
 stands for the proof of that reassociated statement. This keeps complicated assumptions that are
@@ -239,11 +242,7 @@ end
 
 Although `reassoc_of` is not a tactic or a meta program, its type is generated
 through meta-programming to make it usable inside normal expressions.
-
 -/
-theorem category_theory.reassoc_of {α} (hh : α) {β}
-  (x : tactic.calculated_Prop β hh . tactic.derive_reassoc_proof) : β := x
-
 add_tactic_doc
 { name                     := "category_theory.reassoc_of",
   category                 := doc_category.tactic,