判断・主張と質問・問題の区別ができること。 命題と事実と証拠と証明の区別が出来ること。 証明とリーズニングの区別が出来ること。 ローカル前提とグローバル・コンテストの区別が出来ること。 公理や前提と先送りの区別ができること。 コンテスト環境とバ…

ライブラリとバックログは双対的な存在。ライブラリ／パッケージ管理と同程度にバックログ管理機能が必要。現状、何もしてくれない。Idrisのholeがある程度はバックログ管理。

式〈項〉をギリシャ文字で書くとして α providing x:X, y:Y のような形がproviding式。これは、 within {x:X, y:Y} α assuming x:X, y:Y α と同じだが、providing, justificatin は定義義務／証明義務が発生する。providingで導入された宣言は、バックログ（…

翻訳： let → we_have := → by_using, because_of return → we_conclude, we_showed suffice let/return式 let x1: A1 := τ1 let x2: A2 := τ2 ‥‥ return α: C end別な書き方： we_have x1: A1 by_using τ1 we_have x2: A2 by_using τ2 ‥‥ we_conclude C by_…