Foo.add が抜けている

[Seasawher]

6 Lean との対話

現在の名前空間 Foo の中で、コマンド export Nat (succ add sub) は、Nat.succ、Nat.add、Nat.sub に対して別名 Foo.succ、Foo.succ、Foo.sub を生成する。

Foo.add が抜けています．

[aconite-ac]

ご指摘ありがとうございます。 明らかな誤りですので修正いたします。