ドキュメントコメント

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_dsimproc', 'builtin_dsimproc_decl', 'builtin_grind_propagator', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'coinductive', 'declare_command_config_elab', 'declare_config_elab', 'declare_config_getter', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', '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_label_attr', 'register_linter_set', 'register_option', 'register_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 に無視されるわけではなく、他の構文要素と同様にパースされます。したがって特にコードの中で扱うことができます。

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

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: 階乗関数 -/
#doc Nat.factorial

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

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

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)