---
generated_at: 2026-02-19 10:30:00
metrics:
  claims_total: 54
  claims_with_evidence: 54
  claims_without_evidence: 0
confidence_derived: 1.00
---

# 根拠レポート：modules-lang-lean 単体テストケース一覧

## 本レポートについて

### 目的
本レポートは、生成された設計書・ドキュメントの信頼性を検証し、人間レビュアーが効率的にレビューできるようにすることを目的としています。

### チェック方法
以下の観点でドキュメントの内容（Claim：主張）を検証しています：

1. **根拠の有無確認**：各主張に対して、ソースコード・既存設計書・要件定義書などの根拠（Evidence）が存在するか
2. **根拠との整合性**：主張の内容が根拠と矛盾していないか
3. **網羅性**：参照すべき情報源を適切にカバーしているか

### 信頼度スコアの算出
- **confidence_derived** = 根拠あり件数 / 総主張件数
- 状態「○」：根拠あり、「△」：根拠不足または要確認

### 本レポートの使い方
1. まず「サマリー」で全体の信頼度と優先レビュー項目を確認
2. 「Claims と根拠の対応」で △ の項目を重点的にレビュー
3. 「不足情報」で補完が必要な情報源を確認

---

## 1) サマリー（まず見るところ）
- 総合信頼度（derived）：**1.00**
  - 根拠あり：54 / 54、根拠なし：0
- 優先レビュー（高）
  1. **なし**：全テストケースにソースコードの根拠あり

## 2) 参照した情報（Evidence一覧）
> ここに「実在するもの」だけ列挙。抽出フェーズで付けたIDをそのまま出す。

- E-01: `modules/lang/lean/config.el` - Lean言語モジュールの設定ファイル（60行）
- E-02: `modules/lang/lean/doctor.el` - モジュール依存関係チェックファイル（12行）
- E-03: `modules/lang/lean/packages.el` - パッケージ定義ファイル（15行）
- E-04: `modules/lang/lean/README.org` - モジュールドキュメント（67行）

## 3) Claims と根拠の対応（レビューの主戦場）

### config.el - lean-mode (Lean 3 サポート)
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-01 | +v3フラグ有効時にlean-modeが設定される | E-01 (L3-4: `use-package! lean-mode :when (modulep! +v3)`) | ○ |
| C-02 | +v3フラグ無効時にlean-modeがスキップされる | E-01 (L4: `:when (modulep! +v3)`) | ○ |
| C-03 | lean-modeにlookupハンドラが設定される | E-01 (L7-8: `set-lookup-handlers! 'lean-mode :definition #'lean-find-definition`) | ○ |
| C-04 | /-と-/のコメントペアが設定される | E-01 (L10: `sp-local-pair "/-" "-/"`) | ○ |
| C-05 | バッククォートペアが設定される | E-01 (L11: `sp-local-pair "\`" "\`"`) | ○ |
| C-06 | 波括弧ペアが設定される | E-01 (L12: `sp-local-pair "{" "}"`) | ○ |
| C-07 | ギュメペア(guillemets)が設定される | E-01 (L13: `sp-local-pair "«" "»"`) | ○ |
| C-08 | 角括弧ペアが設定される | E-01 (L14: `sp-local-pair "⟨" "⟩"`) | ○ |
| C-09 | 二重角括弧ペアが設定される | E-01 (L15: `sp-local-pair "⟪" "⟫"`) | ○ |
| C-10 | gキーでlean-toggle-show-goalがバインドされる | E-01 (L18: `"g" #'lean-toggle-show-goal`) | ○ |
| C-11 | nキーでlean-toggle-next-errorがバインドされる | E-01 (L19: `"n" #'lean-toggle-next-error`) | ○ |
| C-12 | s rキーでlean-server-restartがバインドされる | E-01 (L21: `"r" #'lean-server-restart`) | ○ |
| C-13 | s sキーでlean-server-stopがバインドされる | E-01 (L22: `"s" #'lean-server-stop`) | ○ |
| C-14 | s vキーでlean-server-switch-versionがバインドされる | E-01 (L23: `"v" #'lean-server-switch-version`) | ○ |
| C-15 | p tキーでlean-leanpkg-testがバインドされる | E-01 (L25: `"t" #'lean-leanpkg-test`) | ○ |
| C-16 | p bキーでlean-leanpkg-buildがバインドされる | E-01 (L26: `"b" #'lean-leanpkg-build`) | ○ |
| C-17 | p cキーでlean-leanpkg-configureがバインドされる | E-01 (L27: `"c" #'lean-leanpkg-configure`) | ○ |
| C-18 | fキーでlean-fill-placeholderがバインドされる | E-01 (L28: `"f" #'lean-fill-placeholder`) | ○ |
| C-19 | hキーでlean-holeがバインドされる | E-01 (L29: `"h" #'lean-hole`) | ○ |
| C-20 | mキーでlean-message-boxes-toggleがバインドされる | E-01 (L30: `"m" #'lean-message-boxes-toggle`) | ○ |
| C-21 | eキーでlean-executeがバインドされる | E-01 (L31: `"e" #'lean-execute`) | ○ |

### config.el - nael (Lean 4 サポート)
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-22 | naelが遅延読み込みで設定される | E-01 (L34-35: `use-package! nael :defer t`) | ○ |
| C-23 | nael-mode-hookにabbrev-modeが追加される | E-01 (L37: `add-hook 'nael-mode-hook #'abbrev-mode`) | ○ |
| C-24 | org-srcにlean言語がnael-modeとしてマッピングされる | E-01 (L38-39: `add-to-list 'org-src-lang-modes '("lean" . nael)`) | ○ |
| C-25 | markdownにlean言語がnael-modeとしてマッピングされる | E-01 (L40-41: `add-to-list 'markdown-code-lang-modes '("lean" . nael-mode)`) | ○ |
| C-26 | nael-modeにコメントペア/-と-/が設定される | E-01 (L44: `sp-local-pair "/-" "-/"`) | ○ |
| C-27 | nael-modeにバッククォートペアが設定される | E-01 (L45: `sp-local-pair "\`" "\`"`) | ○ |
| C-28 | nael-modeに波括弧ペアが設定される | E-01 (L46: `sp-local-pair "{" "}"`) | ○ |
| C-29 | nael-modeにギュメペアが設定される | E-01 (L47: `sp-local-pair "«" "»"`) | ○ |
| C-30 | nael-modeに角括弧ペアが設定される | E-01 (L48: `sp-local-pair "⟨" "⟩"`) | ○ |
| C-31 | nael-modeに二重角括弧ペアが設定される | E-01 (L49: `sp-local-pair "⟪" "⟫"`) | ○ |
| C-32 | +lspフラグ有効時にLSP設定が実行される | E-01 (L50: `when (modulep! +lsp)`) | ○ |
| C-33 | +lspフラグ無効時にLSP設定がスキップされる | E-01 (L50: `when (modulep! +lsp)`) | ○ |
| C-34 | eglot有効時にnael-prepare-lspがnilに設定される | E-01 (L51-52: `if (modulep! :tools lsp +eglot) (setq nael-prepare-lsp nil)`) | ○ |
| C-35 | eglot無効時にnael-prepare-eglotがnilに設定される | E-01 (L53: `(setq nael-prepare-eglot nil)`) | ○ |
| C-36 | nael-mode-local-vars-hookにlsp!が追加される | E-01 (L54: `add-hook 'nael-mode-local-vars-hook #'lsp! 'append`) | ○ |
| C-37 | aキーでnael-abbrev-helpがバインドされる | E-01 (L57: `"a" #'nael-abbrev-help`) | ○ |
| C-38 | bキーでproject-buildがバインドされる | E-01 (L58: `"b" #'project-build`) | ○ |
| C-39 | eキーでeldoc-doc-bufferがバインドされる | E-01 (L59: `"e" #'eldoc-doc-buffer`) | ○ |

### doctor.el - 依存関係チェック
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-40 | +lsp有効時に:tools lspが必要であることが検証される | E-02 (L3-5: `assert! (or (not (modulep! +lsp)) (modulep! :tools lsp))`) | ○ |
| C-41 | +lsp有効で:tools lsp無効時にエラーが発生する | E-02 (L3-5: assert!の条件とメッセージ) | ○ |
| C-42 | +lsp無効時はアサーションが成功する | E-02 (L3: `(not (modulep! +lsp))`がtrueで全体がtrue) | ○ |
| C-43 | lake存在時はエラーが発生しない | E-02 (L7-8: `unless (executable-find "lake")`) | ○ |
| C-44 | lake不在時にエラーメッセージが表示される | E-02 (L8: `error! "lake executable is missing..."`) | ○ |
| C-45 | +v3有効かつlean存在時はエラーが発生しない | E-02 (L10-12: `when (modulep! +v3) (unless (executable-find "lean")`) | ○ |
| C-46 | +v3有効かつlean不在時にエラーメッセージが表示される | E-02 (L12: `error! "lean executable is missing..."`) | ○ |
| C-47 | +v3無効時はleanチェックがスキップされる | E-02 (L10: `when (modulep! +v3)`) | ○ |

### packages.el - パッケージ定義
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-48 | +v3有効時にlean-modeが登録される | E-03 (L4-5: `when (modulep! +v3) (package! lean-mode ...)`) | ○ |
| C-49 | +v3無効時にlean-modeが登録されない | E-03 (L4: `when (modulep! +v3)`) | ○ |
| C-50 | naelパッケージが常に登録される | E-03 (L7: `package! nael ...`) | ○ |
| C-51 | +lspかつ-eglot時にnael-lspが登録される | E-03 (L8-9: `when (and (modulep! +lsp) (modulep! :tools lsp -eglot))`) | ○ |
| C-52 | +lsp無効時にnael-lspが登録されない | E-03 (L8: `modulep! +lsp`がnil) | ○ |
| C-53 | eglot使用時にnael-lspが登録されない | E-03 (L9: `modulep! :tools lsp -eglot`がnil) | ○ |
| C-54 | nael-lspがautoloadsなしでビルドされる | E-03 (L14: `:recipe (:build (:not autoloads))`) | ○ |

## 4) 不足情報（Unknown / Missing）
- 該当なし：全てのテストケースはソースコードから直接抽出されており、根拠が存在する

## 5) リスクフラグ（レビュー観点）
- 0: 低リスク - 全テストケースに明確なソースコード根拠あり
- 注意点：
  - Emacs Lispの単体テストは通常buttercup等のフレームワークを使用するが、現時点でテストコードは存在しない
  - 本テストケース一覧は設計レベルの網羅性を示すものであり、実装レベルのテストコード生成は別途必要

## 6) レビュアーチェックリスト（最小）
- [ ] config.elのlean-mode設定（+v3フラグ条件分岐）が正しくテストされているか確認
- [ ] config.elのnael設定（LSP統合含む）が正しくテストされているか確認
- [ ] doctor.elの依存関係チェック（assert!、executable-find）が網羅されているか確認
- [ ] packages.elのパッケージ登録条件が正しくテストされているか確認
- [ ] キーバインド設定の網羅性を確認（lean-mode: 12個、nael: 3個）
- [ ] smartparensペア設定の網羅性を確認（lean-mode: 6個、nael: 6個）
