タグ🏷️機能を試験的に実装する

Examples/Declarative/DeclareSyntaxCat.lean

@@ -1,5 +1,7 @@
 /- # declare_syntax_cat
 
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `declare_syntax_cat` コマンドは、新しい構文カテゴリを宣言するためのコマンドです。構文カテゴリを宣言することで、宣言した構文を再利用可能にして冗長な構文宣言を減らすことができます。
 
 例として、集合の内包表記 `{x : T | P x}` を定義するコードを示します。

Examples/Declarative/Elab.lean

@@ -1,5 +1,7 @@
 /- # elab
 
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `elab` コマンドは、構文に意味を与えるためのコマンドです。特定の構文の解釈を、手続きとして記述するときに使用されます。
 
 以下の例は、証明が終了したときに 🎉 でお祝いしてくれるタクティクを自作する例です。[^zulip]

Examples/Declarative/Infix.lean

@@ -1,4 +1,7 @@
 /- # infix
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `infix` は、中置記法を定義するコマンドです。
 -/
 import Lean --#

Examples/Declarative/Macro.lean

@@ -1,4 +1,7 @@
 /- # macro
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `macro` は、その名の通りマクロを定義するための簡便なコマンドです。ただしマクロとは、構文を受け取って新しい構文を返す関数のことです。
 -/
 import Mathlib.Data.Real.Sqrt

Examples/Declarative/MacroRules.lean

@@ -1,4 +1,7 @@
 /- # macro_rules
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `macro_rules` はマクロ展開を定めるための汎用的なコマンドです。
 -/
 

Examples/Declarative/Notation.lean

@@ -1,5 +1,7 @@
-/-
-# notation
+/- # notation
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `notation` は、新しい記法を導入するためのコマンドです。
 -/
 

Examples/Declarative/Postfix.lean

@@ -1,4 +1,7 @@
 /- # postfix
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `postfix` は、後置記法を定義するコマンドです。
 -/
 import Lean --#

Examples/Declarative/Prefix.lean

@@ -1,4 +1,7 @@
 /- # prefix
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `prefix` は、前置記法を定義するためのコマンドです。
 -/
 import Lean --#

Examples/Declarative/Syntax.lean

@@ -1,4 +1,7 @@
 /- # syntax
+
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
 `syntax` コマンドは新しい構文を定義することができます。
 -/
 import Lean

Examples/Tactic/WithReducible.lean

@@ -1,7 +1,8 @@
 /- # with_reducible
-`with_reducible` は、後に続くタクティクの透過度(transparency)を `reducible` に指定して実行します。
 
-透過度 `reducible` では、`[reducible]` 属性を持つ定義だけが展開されます。
+[`🏷️メタプログラミング`](./?search=🏷メタプログラミング)
+
+`with_reducible` は、後に続くタクティクの透過度(transparency)を `reducible` に指定して実行します。透過度 `reducible` では、`[reducible]` 属性を持つ定義だけが展開されます。
 
 ## 用途