From cebc301c1167bbfb382b3d697d3766b0c6c5bf02 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Apr 2021 18:14:18 -0700 Subject: [PATCH] chore: remove old test --- tests/lean/envExtensionSealed.lean | 17 ----------------- tests/lean/envExtensionSealed.lean.expected.out | 3 --- 2 files changed, 20 deletions(-) delete mode 100644 tests/lean/envExtensionSealed.lean delete mode 100644 tests/lean/envExtensionSealed.lean.expected.out diff --git a/tests/lean/envExtensionSealed.lean b/tests/lean/envExtensionSealed.lean deleted file mode 100644 index 7899e4f129..0000000000 --- a/tests/lean/envExtensionSealed.lean +++ /dev/null @@ -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 diff --git a/tests/lean/envExtensionSealed.lean.expected.out b/tests/lean/envExtensionSealed.lean.expected.out deleted file mode 100644 index 7a492b0b9f..0000000000 --- a/tests/lean/envExtensionSealed.lean.expected.out +++ /dev/null @@ -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