modify constant by modifying Environment

Stream: new members

[Asei Inoue]

Can we modify declared constant value by modifying Environment?

[Asei Inoue]

for example, can we get hoge = 42 even if it is declared by def hoge := 1, by modifying Environment?

[Henrik Böving]

There are certain hacks that you can do to mutate an Environment in this fashion but this is not something that is generally supported as part of the whole Lean framework no

[Henrik Böving]

In particular changing the definition of a function can make other parts of the env not type check anymore so you can easily get yourself in trouble

[Asei Inoue]

Thank you. so this is possible?
how? (I want to see it for only curiosity)

[Henrik Böving]

It's a bit more difficult with the async Environment etc. now so I don't actually know how to put in into action from the top of my head but the main thing you have to do is modify the kernel environment contained in that thing and then touch the constants map in docs#Lean.Kernel.Environment to do the change you want.