過去の記事をまとめてメモとする。ザッと読んで思い出すには便利だと思う。 シェブロテインのレコーディングフェーズとGAST - (新) 檜山正幸のキマイラ飼育記 メモ編 GAST〈ガスト〉はグラマーASTのこと パーザークラスのコンストラクタが呼ばれると自己分析…

section 分数の定義と掛け算 { declare 0-mor F in Set define F := Int×(Int＼{0}) declare 0-mor 1 in F // オーバーロード define 1 := (1, 1) declare 1-mor m : F×F → F in Set reserve a, b, c ∈F reserve x, y ∈Int define m := λ(a, b).( (a_1×b_1, …

Leanにも、NPMパッケージと同様な仕掛けがあるらしい。 ディレクトリがパッケージ メタデータが leanpkg.toml 一部のメタデータは leanpkg.path にある。 ツールの情報がメタデータに書いてあって、パッケージをダウンロードした先で環境を再現できるように…

まず、以前のLeanを削除する。 elan self uninstall vscodeが上がってたいので、プロセスが使われている云々のエラーが出たが、アンインストールはされた。 https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1 を何でもいいからgetし…