command_elab 属性、あるいは elab コマンドの舞台裏

import Lean

/- Elaboration の流れに沿いつつ、コマンドを自作する例
Lean のユーザは `command_elab` 属性を使ったりする必要はない（ほとんど常に `elab` コマンドと `elab_rules` コマンドで十分）
だが、裏ではこういうことをしている。
-/

open Lean Elab Command Term Meta

-- 1. 構文の定義
syntax (name := mycommand1) "#mycommand1" : command -- declare the syntax

-- 2. エラボレータを定義する
def mycommand1Impl : CommandElab := fun stx => do -- declare and register the elaborator
  logInfo "Hello World"

-- 3. 定義したエラボレータを、特定の構文を扱うものとして登録する
attribute [command_elab mycommand1] mycommand1Impl

#mycommand1 -- Hello World

Start by reviewing the Japanese issue body and its embedded Lean example about the command_elab attribute and elab commands. The payload does not name a target file, test, or explicit completion criterion, so confirm where this documentation belongs and what form the finished addition should take.