diff --git a/Examples/Declarative/DeclareSyntaxCat.lean b/Examples/Declarative/DeclareSyntaxCat.lean
index dbaccb96..eadcbd2a 100644
--- a/Examples/Declarative/DeclareSyntaxCat.lean
+++ b/Examples/Declarative/DeclareSyntaxCat.lean
@@ -1,5 +1,7 @@
 /- # declare_syntax_cat
 
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `declare_syntax_cat` コマンドは、新しい構文カテゴリを宣言するためのコマンドです。構文カテゴリを宣言することで、宣言した構文を再利用可能にして冗長な構文宣言を減らすことができます。
 
 例として、集合の内包表記 `{x : T | P x}` を定義するコードを示します。
diff --git a/Examples/Declarative/Elab.lean b/Examples/Declarative/Elab.lean
index 54d48d09..3164b0ab 100644
--- a/Examples/Declarative/Elab.lean
+++ b/Examples/Declarative/Elab.lean
@@ -1,5 +1,7 @@
 /- # elab
 
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `elab` コマンドは、構文に意味を与えるためのコマンドです。特定の構文の解釈を、手続きとして記述するときに使用されます。
 
 以下の例は、証明が終了したときに 🎉 でお祝いしてくれるタクティクを自作する例です。[^zulip]
diff --git a/Examples/Declarative/Infix.lean b/Examples/Declarative/Infix.lean
index 38d5a48f..a6ea2de5 100644
--- a/Examples/Declarative/Infix.lean
+++ b/Examples/Declarative/Infix.lean
@@ -1,4 +1,7 @@
 /- # infix
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `infix` は、中置記法を定義するコマンドです。
 -/
 import Lean --#
diff --git a/Examples/Declarative/Macro.lean b/Examples/Declarative/Macro.lean
index f45532b8..42674539 100644
--- a/Examples/Declarative/Macro.lean
+++ b/Examples/Declarative/Macro.lean
@@ -1,4 +1,7 @@
 /- # macro
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `macro` は、その名の通りマクロを定義するための簡便なコマンドです。ただしマクロとは、構文を受け取って新しい構文を返す関数のことです。
 -/
 import Mathlib.Data.Real.Sqrt
diff --git a/Examples/Declarative/MacroRules.lean b/Examples/Declarative/MacroRules.lean
index 981d9d57..89efa83c 100644
--- a/Examples/Declarative/MacroRules.lean
+++ b/Examples/Declarative/MacroRules.lean
@@ -1,4 +1,7 @@
 /- # macro_rules
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `macro_rules` はマクロ展開を定めるための汎用的なコマンドです。
 -/
 
diff --git a/Examples/Declarative/Notation.lean b/Examples/Declarative/Notation.lean
index cf4a948a..7c598564 100644
--- a/Examples/Declarative/Notation.lean
+++ b/Examples/Declarative/Notation.lean
@@ -1,5 +1,7 @@
-/-
-# notation
+/- # notation
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `notation` は、新しい記法を導入するためのコマンドです。
 -/
 
diff --git a/Examples/Declarative/Postfix.lean b/Examples/Declarative/Postfix.lean
index 06189712..0cadcce1 100644
--- a/Examples/Declarative/Postfix.lean
+++ b/Examples/Declarative/Postfix.lean
@@ -1,4 +1,7 @@
 /- # postfix
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `postfix` は、後置記法を定義するコマンドです。
 -/
 import Lean --#
diff --git a/Examples/Declarative/Prefix.lean b/Examples/Declarative/Prefix.lean
index 0414d8de..2a7c13df 100644
--- a/Examples/Declarative/Prefix.lean
+++ b/Examples/Declarative/Prefix.lean
@@ -1,4 +1,7 @@
 /- # prefix
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `prefix` は、前置記法を定義するためのコマンドです。
 -/
 import Lean --#
diff --git a/Examples/Declarative/Syntax.lean b/Examples/Declarative/Syntax.lean
index b2e81d14..563790fd 100644
--- a/Examples/Declarative/Syntax.lean
+++ b/Examples/Declarative/Syntax.lean
@@ -1,4 +1,7 @@
 /- # syntax
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `syntax` コマンドは新しい構文を定義することができます。
 -/
 import Lean
diff --git a/Examples/Tactic/WithReducible.lean b/Examples/Tactic/WithReducible.lean
index e77d3e5e..8c3eb711 100644
--- a/Examples/Tactic/WithReducible.lean
+++ b/Examples/Tactic/WithReducible.lean
@@ -1,7 +1,8 @@
 /- # with_reducible
-`with_reducible` は、後に続くタクティクの透過度(transparency)を `reducible` に指定して実行します。
 
-透過度 `reducible` では、`[reducible]` 属性を持つ定義だけが展開されます。
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
+`with_reducible` は、後に続くタクティクの透過度(transparency)を `reducible` に指定して実行します。透過度 `reducible` では、`[reducible]` 属性を持つ定義だけが展開されます。
 
 ## 用途