動画とスライドから

Lean ダメ出し

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 clear

だよね、不明確！

モジュール・インポートの候補としては次があったようだ。実現されなかったが。

import "init/data/set"
import "mathlib/data/set"

名前空間の構造と挙動が分かりにくい。

namespace Nat
 def one := 1
 #eval one -- 1
end Nat
#eval one -- error
#eval Nat.one -- 1
open Nat
namespace Nat
 def one := 1
 #eval one -- 1
end Nat
#eval one -- 1
#eval Nat.one -- 1

なお、特定の名前だけを現名前空間にぶちまけるには open Except (ok error) が使える。