diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 0253c5df6f..040bb5bbf7 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -150,6 +150,9 @@ It can also be written as `()`.
 /-- Marker for information that has been erased by the code generator. -/
 unsafe axiom lcErased : Type
 
+/-- Marker for type dependency that has been erased by the code generator. -/
+unsafe axiom lcAny : Type
+
 /--
 Auxiliary unsafe constant used by the Compiler when erasing proofs from code.