Lean - 版の履歴

2026年5月21日 (木) 16:18にPttによる

2026-05-21T16:18:11Z

← 古い版		2026年5月22日 (金) 01:18時点における版
46行目:		46行目:
	命題		命題

	== ~~キーワード~~ ==		== 証明する ==

	=== by ===		=== 構文 ===
	~~「タクティク」によって証明を開始します~~

	=== ~~intro~~ ===		==== := by ====
	~~intro h~~		証明を開始します

	~~のように書くと、前件~~(A→B においては A)を h という名前で導入します。		=== 定理や仮定を使う ===

			==== rw [h] ====
			h を使ってゴールを書き換えます

			==== intro h ====
			前件(A→B においては A)を h という名前で導入します。

	名前は何でもよく、前から順番に導入されるらしい。		名前は何でもよく、前から順番に導入されるらしい。

	=== exact ===		==== exact h ====
	~~exact h と書くと先ほど導入したh~~ : Aを除去して、A→B を導きます。		先ほど導入したh: Aを除去して、A→B を導きます。

			==== fun ====

			=== 構成的証明 ===

			==== exists A ====
			∃を示すのに、これを満たすAを具体的に指定します

	==~~= fun =~~==		== リンク集 ==
			[https://lean-ja.github.io/lean-by-example/ Lean by Example]

2026-05-21T16:03:37Z

← 古い版		2026年5月22日 (金) 01:03時点における版
16行目:		16行目:
	https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency		https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

	~~※起動時に数分ほどかかりました。~~		lake exe cache get　してビルド済みファイルをダウンロードしておきましょう。
			その後 lean build を実行しておきましょう。

2026-05-21T14:20:03Z

← 古い版		2026年5月21日 (木) 23:20時点における版
6行目:		6行目:

	== インストール ==		== インストール ==
			=== Leanをインストールする ===
	https://lean-lang.org/install/		https://lean-lang.org/install/

14行目:		15行目:
	=== プロジェクトに Mathlib を導入する ===		=== プロジェクトに Mathlib を導入する ===
	https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency		https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

			※起動時に数分ほどかかりました。

2026-05-21T12:36:01Z

← 古い版		2026年5月21日 (木) 21:36時点における版
11行目:		11行目:
	# 適当にファイルを開き、右上のメニューから Lean 4 > New Project... を選択する		# 適当にファイルを開き、右上のメニューから Lean 4 > New Project... を選択する
	# プロジェクトが作られる。必要に応じて色々インストールされる。		# プロジェクトが作られる。必要に応じて色々インストールされる。

			=== プロジェクトに Mathlib を導入する ===
			https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency


	== Lean InfoView ==		== Lean InfoView ==

2026-03-20T03:09:53Z

← 古い版		2026年3月20日 (金) 12:09時点における版
26行目:		26行目:
	=== 定理を証明する ===		=== 定理を証明する ===
	theorem		theorem

			=== 証明する（名前なし） ===
			example

	=== 評価する ===		=== 評価する ===
38行目:		41行目:

	=== by ===		=== by ===
			「タクティク」によって証明を開始します

			=== intro ===
			intro h

	~~=== fun ===~~		のように書くと、前件(A→B においては A)を h という名前で導入します。

	~~=== intro ===~~		名前は何でもよく、前から順番に導入されるらしい。

	=== exact ===		=== exact ===
			exact h と書くと先ほど導入したh : Aを除去して、A→B を導きます。

			=== fun ===

2026-03-16T16:13:31Z

Lean InfoView

← 古い版		2026年3月17日 (火) 01:13時点における版
13行目:		13行目:

	== Lean InfoView ==		== Lean InfoView ==
	~~これを確認するのが目的？~~		これを確認しながら、"Goals accomplished!" を見ることが目標のようです。

	.lean ファイルを開くと自動で開かれる。		.lean ファイルを開くと自動で開かれる。

2026-03-16T16:05:14Z

@@ 1行目: / 1行目: @@
 https://lean-lang.org/
 == インストール ==
@@ 25行目: / 29行目: @@
 === 評価する ===
 <nowiki>#</nowiki>eval

2026-03-16T15:07:09Z

← 古い版		2026年3月17日 (火) 00:07時点における版
14行目:		14行目:

	または、Lean 4 のメニューから Toggle InfoView を選択して開く。		または、Lean 4 のメニューから Toggle InfoView を選択して開く。

			== やること ==

			=== 関数を定義する ===
			def

			=== 定理を証明する ===
			theorem

			=== 評価する ===
			<nowiki>#</nowiki>eval

2026-03-16T15:02:05Z

← 古い版		2026年3月17日 (火) 00:02時点における版
7行目:		7行目:
	# 適当にファイルを開き、右上のメニューから Lean 4 > New Project... を選択する		# 適当にファイルを開き、右上のメニューから Lean 4 > New Project... を選択する
	# プロジェクトが作られる。必要に応じて色々インストールされる。		# プロジェクトが作られる。必要に応じて色々インストールされる。

			== Lean InfoView ==
			これを確認するのが目的？

			.lean ファイルを開くと自動で開かれる。

			または、Lean 4 のメニューから Toggle InfoView を選択して開く。

2026-03-16T14:00:55Z

← 古い版		2026年3月16日 (月) 23:00時点における版
1行目:		1行目:
	https://lean-lang.org/		https://lean-lang.org/

			== インストール ==
			https://lean-lang.org/install/

			# VSCode の拡張機能「Lean 4」をインストールする
			# 適当にファイルを開き、右上のメニューから Lean 4 > New Project... を選択する
			# プロジェクトが作られる。必要に応じて色々インストールされる。