ドキュメントコメント

Lean では、/-- と -/ で囲まれた部分がドキュメントコメントとして扱われます。

ドキュメントコメントは、コードをわかりやすくするのに役立ちます。直後に来る関数や定義を修飾して、そこに書かれた内容がマウスオーバーしたときに表示されます。

/-- 階乗関数 -/
def Nat.factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * Nat.factorial n

なお、「コメント」を「コードの動作に影響を与えない人間向けの説明文」と定義するのであれば、Lean のドキュメントコメントはコメントではありません。誤った場所にドキュメントコメントを配置するとエラーになります。

import Lean

open Lean Parser in

/-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/
def parse (cat : Name) (s : String) : MetaM Syntax := do
  ofExcept <| runParserCategory (← getEnv) cat s

-- ドキュメントコメントで `namespace` を修飾しようとすると構文エラーになる
/-
error: <input>:1:21: expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_cbv_simproc', 'builtin_cbv_simproc_decl', 'builtin_dsimproc', 'builtin_dsimproc_decl', 'builtin_grind_propagator', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'cbv_simproc', 'cbv_simproc_decl', 'class', 'coinductive', 'declare_command_config_elab', 'declare_command_config_elab_legacy', 'declare_config_elab', 'declare_config_elab_legacy', 'declare_core_config_elab', 'declare_simp_like_tactic', 'declare_syntax_cat', 'declare_term_config_elab', 'def', 'def_eval_config_item', 'dsimproc', 'dsimproc_decl', 'elab', 'elab_rules', 'example', 'grind_propagator', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'recommended_spelling', 'register_builtin_option', 'register_error_explanation', 'register_grind_attr', 'register_label_attr', 'register_linter_set', 'register_option', 'register_simp_attr', 'register_sym_simp_attr', 'register_tactic_tag', 'register_try?_tactic', 'simproc', 'simproc_decl', 'structure', 'syntax', 'tactic_extension', 'theorem' or 'unif_hint'
-/
#eval parse `command "/-- これはドキュメントコメント -/ namespace Foo"

ドキュメントコメントを扱う例

ドキュメントコメントは Lean に無視されるわけではなく、他の構文要素と同様にパースされます。したがって特にコードの中で扱うことができます。

たとえば、ドキュメントコメントを取得して内容を表示するコマンドを書くことができます。

import Lean.Elab.Command

open Lean Elab Command in

/-- ドキュメントコメントを取得して表示するコマンド -/
elab "#doc " x:ident : command => do
  let name := x.getId
  if let some s ← findDocString? (← getEnv) name then
    logInfo m!"{s}"

/-
info: Linked lists: ordered lists, in which each element has a reference to the next element.

Most operations on linked lists take time proportional to the length of the list, because each
element must be traversed to find the next element.

`List α` is isomorphic to `Array α`, but they are useful for different things:
* `List α` is easier for reasoning, and `Array α` is modeled as a wrapper around `List α`.
* `List α` works well as a persistent data structure, when many copies of the tail are shared. When
  the value is not shared, `Array α` will have better performance because it can do destructive
  updates.
-/
#doc List

補足：コメントはパースされている

なお、ドキュメントコメントに限らず、Lean のコメントはパーサに無視されません。ただ実行内容を持たず、コードの動作に影響を与えないだけです。

import Lean.Elab.Command

open Lean Elab Command Parser

/-
info: def foo :
    -- ここにコメント
    /- ここにもコメント -/
    True :=
  trivial
-/
run_cmd liftTermElabM do
  let s := "def foo : \n\
    -- ここにコメント\n\
    /- ここにもコメント -/\n\
    True := trivial"
  let cmd : Command := ⟨← ofExcept <| runParserCategory (← getEnv) `command s⟩
  logInfo (← PrettyPrinter.ppCommand cmd)