証明図〈横棒図〉やストリング図を扱うこと、解釈すること。 順行リーズニング 柔軟な参照（固有名、固有ラベル以外の参照方法） 直示 位置による参照 曖昧参照 リーズニングの中断保留（未完成のままに保存） 順行リーズニングと逆行リーズニングを混ぜたリ…

命題の真偽判定： 白黒つける、決着をつける。どうやって？ 証明項の正当性検証： 構文を決めれば機械的に決定出来るか、または無限走行 証明項の生成工程〈リーズニングプロセス〉の正当性検証： 構文を決めれば機械的に決定出来るか、または無限走行 証明…

問題は、絵図で自明なことをどうやってテキストエンコードするか？ 論理絵図＝横棒図〈バー図〉 圏論絵図＝ストリング図 テキスト 論理絵図 圏論絵図 命題 命題 ワイヤー・ラベル 証拠ラベル バー・ラベル ノード・ラベル 証明項 横棒図 ストリング図 公理 …

次が基本概念： 色々なレベルのコンテキスト ステージ（リーズニングの状態） フォーカス（リーズニング中に注目している判断または問題） ターゲット（判断または問題の項と型） コンテキストには： ライブラリ（知識ベース）のコンテキスト ステージのコン…

#eval で値〈要素〉を表示するには、型が型クラス Repr の型インスタンスでなくてはならない。文字列化できるためには、型が型クラス ToStrng の型インスタンスでなくてはならない。

バージョン 3 の lean 3.23.0 lean.exe leanchecker.exe leanpkg leanpkg.bat libgcc_s_seh-1.dll libgmp-10.dll libstdc++-6.dll libwinpthread-1.dll バージョン4のクリスマスイブ版 nightly-2022-12-24 clang.exe lake.exe ld.lld.exe lean.exe leanc.exe…

https://www.youtube.com/watch?v=QI-fEXSX1BA 2分30秒くらい progress has been super-slow. 進捗は非常に遅い、と。https://leanprover.github.io/talks/vu2019.pdf P.9 ： Connection between modules, packages, and namespaces in Lean 3 is not very c…

def f1 : Nat → Nat → Nat := by exact (fun (n m: Nat) => n + m) #check f1 def f2 (n: Nat): Nat → Nat := by intro m exact n + m #check f2 def f3 (n m: Nat): Nat := by exact n + m #check f3

Leanサーバーは、環境変数LEAN_PATHなしでも、./lake-packages/some-package/build/lib/ の下を見ることは知っているようだ。import Foo は ./lake-packages/some-package/build/lib/Foo.olean をロードする。Lean.findOLean が役に立つ。 #eval Lean.findOL…

lean_packages/ が lake-packages/ になった。 lean_packages/manifest.json が lean-manifest.json になった。 属性 @[defaultTarget ...] が @[default_target ...] になった。 lean-toolchain がなくてもよかったが、ほぼ必須になった。ない場合はたぶん…

一般 抽象的 Lean 具体的 ライブラリコンテキスト プレリュードとインストールしたパッケージ達 ワーキングコンテキスト モジュール／名前空間／セクションのコンテキスト 質問コンテキスト 未証明定理の前提 判断コンテキスト 既証明定理の前提

コンテキストの階層は、外から内に向かって： ライブラリコンテキスト＝知識ベース ワーキングコンテキスト＝ステージコンテキスト 判断コンテキスト または 問題コンテキスト コンテキスト＝混合コンテキストには次のものが格納される。情報の重複がある。…

これって、昔Catyでやろうとしていたこと（一部はやった）ことだ。 structure LatticePoint2D where x: Int y: Int #check LatticePoint2D def LatticePoint2D.moveBy (p : LatticePoint2D) (u v:Int) : LatticePoint2D := { x := p.x + u y := p.y + v } #c…

次の3つを混同しない！ 定理のボディ（関数定義のボディ相当） 証明項 リーズニング リーズニング： バックワード フォワード 背景知識ベース 背景知識ベース リーズニング・ステージ リーズニング・ステージ ステージ・コンテキスト ステージ・コンテキスト…

cat lean-toolchain elan toolchain list elan show だとダウンロードが始まる cat lakefile.lean cat .git/HEAD デタッチされているか？ git branch git rev-parse カレントブランチ git tag git rev-parse $(git tag | tail -1) git log --oneline git rev…

Powershell では、foo |& bar も foo 2>&1 | bar も効かない。標準エラー出力を tee でファイルに落とすのは現状分からない。bashなら次が出来るが、Powershellの代替は見つからないでいる。 lake build -v |& tee $(date +%Y-%m-%d_%H-%M-%S).lake-build.log

次のパッケージをトップレベルパッケージ（依存パッケージではなく）git clone でインストールする。 "leancolls" : https://github.com/jamesgallicchio/leancolls インストールしてすぐ気がつくのは： ./lean_packages/ というディレクトリがある。./lake-…