From b7815b56843f5da8ce9d31bbf9d53a2f5ce2a85d Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Thu, 16 Jan 2025 17:33:35 -0800 Subject: [PATCH] feat: add lcAny constant to Prelude (#6665) This PR adds a new lcAny constant to Prelude, which is meant for use in LCNF to represent types whose dependency on another term has been erased during compilation. This is in addition to the existing lcErased constant, which represents types that are irrelevant. --- src/Init/Prelude.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 0253c5df6fa0..040bb5bbf7a4 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.