From ee59048bfbc673ce0f7240e8b57d9cdcb5755310 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 5 Oct 2022 05:09:19 -0700
Subject: [PATCH] chore: remove dead declaration

We have merged `lcErased` and `lcAny` in the new code generator.
---
 src/Init/Prelude.lean     | 3 ---
 tests/lean/lcnfTypes.lean | 1 -
 2 files changed, 4 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 09138bf7ed..7d7f55ce62 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -137,9 +137,6 @@ It can also be written as `()`.
 /-- Marker for information that has been erased by the code generator. -/
 unsafe axiom lcErased : Type
 
-/-- "Any" type in the simpler type system used by the code generator. -/
-unsafe axiom lcAny : Type
-
 /--
 Auxiliary unsafe constant used by the Compiler when erasing proofs from code.
 
diff --git a/tests/lean/lcnfTypes.lean b/tests/lean/lcnfTypes.lean
index 3fbf4f118f..f5f35191d6 100644
--- a/tests/lean/lcnfTypes.lean
+++ b/tests/lean/lcnfTypes.lean
@@ -1,7 +1,6 @@
 import Lean
 
 notation "◾" => lcErased
-notation "⊤" => lcAny
 
 open Lean Compiler LCNF Meta