Skip to content

Commit

Permalink
feat: add lcAny constant to Prelude (#6665)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
zwarich authored Jan 17, 2025
1 parent 7f0ae22 commit b7815b5
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions src/Init/Prelude.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit b7815b5

Please sign in to comment.