feat: make Environment.mk private#2604
Conversation
|
|
How can I obtain an empty Environment for mock testing? |
Would using |
Interesting, just learned that private is not definite Lean. |
@SchrodingerZhu, sorry, I gave you the wrong answer previously: you can use |
|
Making In order to keep things moving, I'm now going to revert the commit to this PR in which I made |
This reverts commit ec12d6b.
|
@digama0, if you're happy with my proposed change to the comment, I can merge this. |
|
Hm, the |
The interpreter only knows how to handle |
|
My suggestion is that we merge as is, and then when #2617 is merged Aesop can use that, and then we can make |
As one follow-up to the discussion here and here, one easy way to make it harder for tactic-writers to accidentally modify the environment to add unchecked constants is to make the constructor private.
Against my expectations, this broke literally nothing in lean itself, and only one test (which ironically was testing private constructors); this was switched to use the API function and everything else worked. We'll see what the mathlib breakage is.