test: Environment.addExtraName

src/Lean/Environment.lean

@@ -19,6 +19,8 @@ def EnvExtensionState : Type := EnvExtensionStateSpec.fst
 instance : Inhabited EnvExtensionState := EnvExtensionStateSpec.snd
 
 def ModuleIdx := Nat
+  deriving BEq, ToString
+
 abbrev ModuleIdx.toNat (midx : ModuleIdx) : Nat := midx
 
 instance : Inhabited ModuleIdx := inferInstanceAs (Inhabited Nat)

tests/pkg/misc/Misc.lean

@@ -0,0 +1,11 @@
+import Misc.Foo
+import Lean
+
+open Lean Meta
+
+#eval id (α := MetaM Unit) do
+  assert! (← getEnv).getModuleIdxFor? ``foo == (← getEnv).getModuleIdxFor? `auxDecl1
+  IO.println <| (← getEnv).getModuleIdxFor? ``Lean.Environment
+  IO.println <| (← getEnv).getModuleIdxFor? ``foo
+  IO.println <| (← getEnv).getModuleIdxFor? `auxDecl1
+  IO.println "worked"

tests/pkg/misc/Misc/Foo.lean

@@ -0,0 +1,9 @@
+import Lean
+
+open Lean Meta
+
+#eval id (α := MetaM Unit) do
+  modifyEnv fun env => env.addExtraName `auxDecl1
+  return ()
+
+def foo := 42

tests/pkg/misc/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package misc
+@[defaultTarget] lean_lib Misc

tests/pkg/misc/test.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+rm -rf build
+lake build