chore: remove old test

2021-04-22 18:14:18 -07:00 · 2021-04-22 18:14:18 -07:00 · cebc301c11
commit cebc301c11
parent 61259697bd
2 changed files with 0 additions and 20 deletions
--- a/tests/lean/envExtensionSealed.lean
+++ b/tests/lean/envExtensionSealed.lean
@ -1,17 +0,0 @@
-import Lean
-
-namespace Lean
-
-def ex1 : CoreM Nat := do
-let env ← getEnv
-pure $ privateExt.getState env
-
-#eval ex1
-
-def ex2 : CoreM Nat := do
-let env ← getEnv
-pure $ { privateExt with idx := 3 }.getState env  -- Error
-
-- #eval ex2
-
-end Lean
--- a/tests/lean/envExtensionSealed.lean.expected.out
+++ b/tests/lean/envExtensionSealed.lean.expected.out
@ -1,3 +0,0 @@
-1
-envExtensionSealed.lean:13:7-13:35: error: invalid {...} notation, source type is not of the form (C ...)
-  EnvExtensionInterfaceImp.1 Nat