From 1fb112f84be76d2ec4c365ef3a9cc3a6e2838215 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Sep 2022 15:03:11 -0700 Subject: [PATCH] test: `Environment.addExtraName` --- src/Lean/Environment.lean | 2 ++ tests/pkg/misc/Misc.lean | 11 +++++++++++ tests/pkg/misc/Misc/Foo.lean | 9 +++++++++ tests/pkg/misc/lakefile.lean | 5 +++++ tests/pkg/misc/test.sh | 4 ++++ 5 files changed, 31 insertions(+) create mode 100644 tests/pkg/misc/Misc.lean create mode 100644 tests/pkg/misc/Misc/Foo.lean create mode 100644 tests/pkg/misc/lakefile.lean create mode 100755 tests/pkg/misc/test.sh diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index d3441abcbb..8db5f6778c 100644 --- a/src/Lean/Environment.lean +++ b/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) diff --git a/tests/pkg/misc/Misc.lean b/tests/pkg/misc/Misc.lean new file mode 100644 index 0000000000..ec165e72ce --- /dev/null +++ b/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" diff --git a/tests/pkg/misc/Misc/Foo.lean b/tests/pkg/misc/Misc/Foo.lean new file mode 100644 index 0000000000..077786d034 --- /dev/null +++ b/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 diff --git a/tests/pkg/misc/lakefile.lean b/tests/pkg/misc/lakefile.lean new file mode 100644 index 0000000000..dfd791ca28 --- /dev/null +++ b/tests/pkg/misc/lakefile.lean @@ -0,0 +1,5 @@ +import Lake +open System Lake DSL + +package misc +@[defaultTarget] lean_lib Misc diff --git a/tests/pkg/misc/test.sh b/tests/pkg/misc/test.sh new file mode 100755 index 0000000000..438bb1c522 --- /dev/null +++ b/tests/pkg/misc/test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +rm -rf build +lake build