meta keyword in Lean 4

Stream: general

[Asei Inoue]

meta keyword will come back?

https://github.com/leanprover/lean4/commit/8457342d335edc5863f4682f8561d6ce93966e2a

[Aaron Liu]

What will it do?

[Asei Inoue]

The keyword meta has been currently removed from Lean 4. However, we may re-introduce it in the future, but with a much more limited purpose: marking meta code that should not be included in the executables produced by Lean.

https://lean-lang.org/lean4/doc/lean3changes.html#the-meta-keyword

[Asei Inoue]

In what situations is meta keyword necessary?

[Kevin Buzzard]

It's not necessary in any situations because it doesn't exist

[Asei Inoue]

will be necessary?

[Robin Arnez]

I think it's part of the module system, so it won't be necessary usually

[Marc Huisinga]

See also lean4#8660