Lean

Ptt — Thu, 21 May 2026 16:18:11 GMT

← 古い版		2026年5月22日 (金) 01:18時点における版
(同じ利用者による、間の3版が非表示)
6行目:		6行目:

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

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

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

			lake exe cache get　してビルド済みファイルをダウンロードしておきましょう。
			その後 lean build を実行しておきましょう。


	== Lean InfoView ==		== Lean InfoView ==
38行目:		46行目:
	命題		命題

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

			=== 構文 ===

			==== := by ====
			証明を開始します

	=== by ===		=== 定理や仮定を使う ===
	~~「タクティク」によって証明を開始します~~

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

	~~のように書くと、前件~~(A→B においては A)を 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]

ペチラボ書庫 - 最近の更新 [ja]

Lean