Deactivate the standard library

Stream: new members

[tica]

The types nat, bool etc are still available.
Is it possible to disable them to have a clean version with 0 libraries?

Thanks

[Johan Commelin]

Start the top of your file with prelude.

[tica]

Thank you

[Eric Wieser]

Note that if you do this you won't even have = (docs#eq) or the tactic framework (docs#tactic.step)

[tica]

@Eric Wieser Yes I know and that's the point.

I would like to see exactly what is defined in lean and is part of the standard library and what is part of the core in C++.

I'm not sure if this is a good idea because I'm already stuck.

What is the quotient module? init_quotient
I guess it must be C++ code.

[Eric Wieser]

I would like to see exactly what is defined in lean and is part of the standard library and what is part of the core in C++.

Unfortunately to actually use the (meta) things in the core C++, you need to add the meta constant declarations in the Lean code.

[Eric Wieser]

See for instance src#tactic.set_goals

[tica]

@Eric Wieser Yes, I think I understood correctly, this is what allows us to make tactics.

The init_quotient, what is it?

I just want to understand better how lean works

[Eric Wieser]

It comes from here, and is a "command" like "def" or "theorem": https://github.com/leanprover-community/lean/blob/34f41e59146bbda3b58adb23dff350c30093e02b/src/frontends/lean/builtin_cmds.cpp#L695

[tica]

@Eric Wieser Thank you!
That's what I thought (that it was C++ code).

I will try to dive into the code ^^