doc(*): work around markdown2 bug for now (#4842)

Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

src/category_theory/natural_isomorphism.lean

@@ -14,12 +14,13 @@ For the most part, natural isomorphisms are just another sort of isomorphism.
 We provide some special support for extracting components:
 * if `α : F ≅ G`, then `a.app X : F.obj X ≅ G.obj X`,
 and building natural isomorphisms from components:
-* ```
-  nat_iso.of_components
-    (app : ∀ X : C, F.obj X ≅ G.obj X)
-    (naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) :
-  F ≅ G
-  ```
+*
+```
+nat_iso.of_components
+  (app : ∀ X : C, F.obj X ≅ G.obj X)
+  (naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) :
+F ≅ G
+```
 only needing to check naturality in one direction.
 
 ## Implementation

src/control/monad/writer.lean

@@ -77,16 +77,18 @@ end
 end writer_t
 
 
-/-- An implementation of [MonadReader](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Reader-Class.html#t:MonadReader).
-    It does not contain `local` because this function cannot be lifted using `monad_lift`.
-    Instead, the `monad_reader_adapter` class provides the more general `adapt_reader` function.
-
-    Note: This class can be seen as a simplification of the more "principled" definition
-    ```
-    class monad_reader (ρ : out_param (Type u)) (n : Type u → Type u) :=
-    (lift {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α) → n α)
-    ```
-    -/
+/--
+An implementation of [MonadReader](
+https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Reader-Class.html#t:MonadReader).
+It does not contain `local` because this function cannot be lifted using `monad_lift`.
+Instead, the `monad_reader_adapter` class provides the more general `adapt_reader` function.
+
+Note: This class can be seen as a simplification of the more "principled" definition
+```
+class monad_reader (ρ : out_param (Type u)) (n : Type u → Type u) :=
+(lift {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α) → n α)
+```
+-/
 class monad_writer (ω : out_param (Type u)) (m : Type u → Type v) :=
 (tell (w : ω) : m punit)
 (listen {α} : m α → m (α × ω))

src/tactic/localized.lean

@@ -12,24 +12,24 @@ This consists of two user-commands which allow you to declare notation and comma
 namespace.
 
 * Declare notation which is localized to a namespace using:
-  ```lean
-  localized "infix ` ⊹ `:60 := my_add" in my.add
-  ```
+```lean
+localized "infix ` ⊹ `:60 := my_add" in my.add
+```
 * After this command it will be available in the same section/namespace/file, just as if you wrote
   `local infix ` ⊹ `:60 := my_add`
 * You can open it in other places. The following command will declare the notation again as local
   notation in that section/namespace/files:
-  ```lean
-  open_locale my.add
-  ```
+```lean
+open_locale my.add
+```
 * More generally, the following will declare all localized notation in the specified namespaces.
-  ```lean
-  open_locale namespace1 namespace2 ...
-  ```
+```lean
+open_locale namespace1 namespace2 ...
+```
 * You can also declare other localized commands, like local attributes
-  ```lean
-  localized "attribute [simp] le_refl" in le
-  ```
+```lean
+localized "attribute [simp] le_refl" in le
+```
 The code is inspired by code from Gabriel Ebner from the
 [hott3 repository](https://github.com/gebner/hott3).
 -/
@@ -81,41 +81,41 @@ This consists of two user-commands which allow you to declare notation and comma
 namespace.
 
 * Declare notation which is localized to a namespace using:
-  ```lean
-  localized "infix ` ⊹ `:60 := my_add" in my.add
-  ```
+```lean
+localized "infix ` ⊹ `:60 := my_add" in my.add
+```
 
 * After this command it will be available in the same section/namespace/file, just as if you wrote
   `local infix ` ⊹ `:60 := my_add`
 
 * You can open it in other places. The following command will declare the notation again as local
   notation in that section/namespace/files:
-  ```lean
-  open_locale my.add
-  ```
+```lean
+open_locale my.add
+```
 
 * More generally, the following will declare all localized notation in the specified namespaces.
-  ```lean
-  open_locale namespace1 namespace2 ...
-  ```
+```lean
+open_locale namespace1 namespace2 ...
+```
 
 * You can also declare other localized commands, like local attributes
-  ```lean
-  localized "attribute [simp] le_refl" in le
-  ```
+```lean
+localized "attribute [simp] le_refl" in le
+```
 
 * To see all localized commands in a given namespace, run:
-  ```lean
-  run_cmd print_localized_commands [`my.add].
-  ```
+```lean
+run_cmd print_localized_commands [`my.add].
+```
 
 * To see a list of all namespaces with localized commands, run:
-  ```lean
-  run_cmd do
-    m ← localized_attr.get_cache,
-    tactic.trace m.keys -- change to `tactic.trace m.to_list`
-    -- to list all the commands in each namespace
-  ```
+```lean
+run_cmd do
+  m ← localized_attr.get_cache,
+  tactic.trace m.keys -- change to `tactic.trace m.to_list`
+  -- to list all the commands in each namespace
+```
 
 * Warning 1: as a limitation on user commands, you cannot put `open_locale` directly after your
   imports. You have to write another command first (e.g. `open`, `namespace`, `universe variables`,

src/tactic/simps.lean

@@ -99,17 +99,17 @@ attribute [notation_class* coe_fn] has_coe_to_fun
     corresponding projection
   * Otherwise, the projection of the structure is chosen.
     For example: ``simps_get_raw_projections env `prod`` gives the default projections
-    ```
-      ([u, v], [prod.fst.{u v}, prod.snd.{u v}])
-    ```
+```
+  ([u, v], [prod.fst.{u v}, prod.snd.{u v}])
+```
     while ``simps_get_raw_projections env `equiv`` gives
-    ```
-      ([u_1, u_2], [λ α β, coe_fn, λ {α β} (e : α ≃ β), ⇑(e.symm), left_inv, right_inv])
-    ```
+```
+  ([u_1, u_2], [λ α β, coe_fn, λ {α β} (e : α ≃ β), ⇑(e.symm), left_inv, right_inv])
+```
     after declaring the coercion from `equiv` to function and adding the declaration
-    ```
-      def equiv.simps.inv_fun {α β} (e : α ≃ β) : β → α := e.symm
-    ```
+```
+  def equiv.simps.inv_fun {α β} (e : α ≃ β) : β → α := e.symm
+```
 
   Optionally, this command accepts two optional arguments
   * If `trace_if_exists` the command will always generate a trace message when the structure already