From 366a0c90a2799828982a305b2d045f4fe8f2a1a0 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 17 Nov 2024 00:56:12 +0900
Subject: [PATCH] =?UTF-8?q?#version=20=E3=82=B3=E3=83=9E=E3=83=B3=E3=83=89?=
 =?UTF-8?q?=E3=82=92=E7=B4=B9=E4=BB=8B=E3=81=99=E3=82=8B=20Fixes=20#1116?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/Diagnostic/Version.lean | 6 ++++++
 booksrc/SUMMARY.md                              | 1 +
 2 files changed, 7 insertions(+)
 create mode 100644 LeanByExample/Reference/Diagnostic/Version.lean

diff --git a/LeanByExample/Reference/Diagnostic/Version.lean b/LeanByExample/Reference/Diagnostic/Version.lean
new file mode 100644
index 0000000..ecb363d
--- /dev/null
+++ b/LeanByExample/Reference/Diagnostic/Version.lean
@@ -0,0 +1,6 @@
+/- # \#version
+
+`#version` コマンドは、その環境での Lean のバージョンと OS の情報を表示します。
+-/
+
+#version
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index 2efcde6..e566d3f 100644
--- a/booksrc/SUMMARY.md
+++ b/booksrc/SUMMARY.md
@@ -21,6 +21,7 @@
   - [#reduce: 式を簡約する](./Reference/Diagnostic/Reduce.md)
   - [#synth: 型クラスの検査](./Reference/Diagnostic/Synth.md)
   - [#time: 実行時間計測](./Reference/Diagnostic/Time.md)
+  - [#version: バージョン表示](./Reference/Diagnostic/Version.md)
   - [#whnf: 式を弱頭正規形に](./Reference/Diagnostic/Whnf.md)
 
 - [宣言的コマンド](./Reference/Declarative/README.md)