🔰Lean4でスタンダードライブラリを無効化する方法はありますか？

[LumaKernel]

なるべくブラックボックスをなくして、基礎に近い数学の学習とともにLean4の学習も伏せてやりたいというモチベーションがあります。

定義ジャンブを用いれば定義された記法(syntaxやmacro?)なのかどうかというのは辿れそうではあるのですが、そもそもそういったスタンダードライブラリなしで使えるモードなどはないのかなと思いまして…MyNatのように名前よけをするのも少し煩わしいかなと思いました。
感覚としては、Rustのno std環境などに近いかもしれません。
例えば集合論の組み立てから行いたいときに、デフォルトで入っている記法は上書きして使いたいし、自分で揃えたい、といったことは叶えられるのか…気になりました。
まだこれから勉強しようというところなので根本的な勘違い等ありましたらご指摘いただけますと幸いです。(スコープ分ける方法があってそれ使えば一発で解決する…など)

[Seasawher]

コメントありがとうございます

既存の定義との名前被りを避ける方法としては、namespace を使うのが一般的だと思います

数学系のためのlean勉強会でも、Tutorial という名前空間を開くことで名前被りを避けていました。
https://github.com/yuma-mizuno/lean-math-workshop/blob/master/Tutorial/Basic/Lecture4.lean#L7

おそらくこれが求められているものではないかなと思います

[Seasawher]

例えば集合論の組み立てから行いたいときに、デフォルトで入っている記法は上書きして使いたいし、自分で揃えたい、

先述の「数学系のためのlean勉強会」がまさにこれを行なっているので、コードをご覧になると参考になるのではと思います。

[LumaKernel]

ありがとうございます。求めていたものに近そうです。見てみます

[LumaKernel]

yoshidajさんより

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/undefine.20or.20hide.20core.20library.3F

prelude が使えるという情報をいただきました。