syntax コマンドを紹介する

Fixes #622

Examples/Command/Declarative/Syntax.lean

@@ -0,0 +1,31 @@
+/- # syntax
+`syntax` コマンドは新しい構文を定義することができます。
+-/
+import Lean
+
+open Lean Parser
+
+/-- parse できるかどうかチェックする関数 -/
+def checkParse (cat : Name) (s : String) : MetaM Unit := do
+  if let .error s := runParserCategory (← getEnv) cat s then
+    throwError s
+
+-- 最初は `#greet` などというコマンドは定義されていないので
+-- そもそも Lean の合法な構文として認められない。
+/-- error: <input>:1:0: expected command -/
+#guard_msgs (error) in
+  #eval checkParse `command "#greet"
+
+-- `#greet` というコマンドのための構文を定義
+syntax "#greet" : command
+
+-- `#greet` というコマンドが Lean に認識されるようになった。
+-- エラーメッセージは、`#greet` コマンドの解釈方法がないと言っている。
+/-- error: elaboration function for '«command#greet»' has not been implemented -/
+#guard_msgs in #greet
+
+/- Lean に構文を認識させるだけでなく、解釈させるには [`macro_rules`](./MacroRules.md) などの別のコマンドが必要です。-/
+
+-- `#greet` コマンドの解釈方法を定める
+macro_rules
+  | `(command| #greet) => `(#eval "Hello, Lean!")

src/SUMMARY.md

@@ -51,6 +51,7 @@
     - [section: スコープを区切る](./Command/Declarative/Section.md)
     - [set_option: オプション設定](./Command/Declarative/SetOption.md)
     - [structure: 構造体を定義する](./Command/Declarative/Structure.md)
+    - [syntax: 構文を定義](./Command/Declarative/Syntax.md)
     - [termination_by: 整礎再帰を使う](./Command/Declarative/TerminationBy.md)
     - [theorem: 命題を証明する](./Command/Declarative/Theorem.md)
     - [variable: 引数を共通化する](./Command/Declarative/Variable.md)