属性を [ ] で囲っていない箇所がある

Examples/Attribute/InductionEliminator.lean

@@ -62,7 +62,7 @@ example (xs : Many α) : Many.union xs Many.none = xs := by
 
     simp [Many.union, Many.cons, ih]
 
-/- `induction_eliminator` を設定する前の挙動に戻すには、`using` キーワードに明示的に `.rec` 定理を与えます。 -/
+/- `[induction_eliminator]` を設定する前の挙動に戻すには、`using` キーワードに明示的に `.rec` 定理を与えます。 -/
 
 example (xs : Many α) : True := by
   -- 明示的に指定すれば， 元の挙動に戻せる

Examples/Attribute/InheritDoc.lean

@@ -26,7 +26,7 @@ end
 /-- info: 最初に与えた doc コメント -/
 #guard_msgs in #doc greet'
 
-/- `inherit_doc` を使用するのは、記法を導入する際であることが多いでしょう。この場合、ドキュメントコメントの継承元を指定する必要がありません。 -/
+/- `[inherit_doc]` 属性を使用するのは、記法を導入する際であることが多いでしょう。この場合、ドキュメントコメントの継承元を指定する必要がありません。 -/
 
 /-- `⊔` という記号のための型クラス -/
 class Sup (α : Type) where

Examples/Attribute/Simps.lean

@@ -4,7 +4,7 @@
 
 例えば、ユーザが `Point` という構造体を定義し、`Point` 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「`Point` の和の `x` 座標」は `x` 座標の和ですが、これはそのままでは `simp` で示すことができません。`[simps]` 属性を `Point.add` 関数に付与することで、`simp` で示せるようになります。
 -/
-import Mathlib.Tactic.Simps.Basic -- simps 属性を使うため
+import Mathlib.Tactic.Simps.Basic -- [simps] 属性を使うため
 
 @[ext]
 structure Point where

Examples/Declarative/Local.lean

@@ -102,7 +102,7 @@ theorem MyNat.zero_add (n : MyNat) : MyNat.add .zero n = n := by
   | succ n ih => simp [MyNat.add, ih]
 
 section
-  -- simp 属性をローカルに付与する
+  -- [simp] 属性をローカルに付与する
   attribute [local simp] MyNat.zero_add
 
   -- その section の中では使用できる

Examples/Tactic/WithReducible.lean

@@ -1,7 +1,7 @@
 /- # with_reducible
 `with_reducible` は、後に続くタクティクの透過度(transparency)を `reducible` に指定して実行します。
 
-透過度 `reducible` では、`[reducible]` の属性を持つ定義だけが展開されます。
+透過度 `reducible` では、`[reducible]` 属性を持つ定義だけが展開されます。
 
 ## 用途