diff --git a/Examples/Tactic/SeqFocus.lean b/Examples/Tactic/SeqFocus.lean
index d21cc62e..62f9de91 100644
--- a/Examples/Tactic/SeqFocus.lean
+++ b/Examples/Tactic/SeqFocus.lean
@@ -1,5 +1,5 @@
 /- # <;>
-`<;>` (seq focus)は、直前のタクティクによって生成されたすべてのサブゴールに対して後続のタクティクを適用することを意味するタクティク結合子です。
+`<;>` は、直前のタクティクによって生成されたすべてのサブゴールに対して後続のタクティクを適用することを意味するタクティク結合子です。[^name]
 -/
 
 variable (P Q : Prop)
@@ -37,3 +37,5 @@ example (hP : P) (hQ : Q) (hR : R) : (P ∧ Q) ∧ R := by
 
   -- 証明完了
   done
+
+/- [^name]: `<;>` の正式な呼び名はわかりません。`linter.unnecessarySeqFocus` というリンタが存在するので、ここでは `seqFocus` と仮に呼んでいます。-/