混合コンテキストが、次のレベルで提供される。 ライブラリ パッケージ モジュール 名前空間 セクション 関数・定理（のボディブロック） 入れ子ブロック（by, doなど） これらの組織化機構〈organizing mechanism / feature〉は独立ではないし、一様でもな…

コード編集中に[F5]でデバッグモードになるが、Leanの場合は、デバッガやそのVSCode拡張が存在しないので、[F5]は効かない。

例： attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_commルート名前空間は無名だが、_root_ という名前で参照できる。

まず、 $ git clone https://github.com/xubaiw/Socket.lean $ cd Socket.lean $ cat lean-toolchain leanprover/lean4:nightly-2022-06-16 去年だと、「ふるっ！」と思う。 $ git branch * main $ git rev-parse main 9fc98bc24ccdb4471b2e38e94dccd18f75d2…

コントロール＋クリック "Cli" : https://github.com/mhuisi/lean4-cli 非依存 "leancolls" : https://github.com/jamesgallicchio/leancolls mathlib依存、ビルド失敗 "advent" : https://github.com/odomontois/advent2022-lean mathlib依存、ビルド成功 "…

npmのpackage-lock.json相当が、Lakeマニフェストファイル。lean_packages/manifes.json と lake-manifest.json がある。注意すべきはマニフェストファイル自体のバージョンで、JSONファイルのトップレベルフィールドとしてバージョン番号が記入されている。…