max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove dead declaration

Browse source 
We have merged `lcErased` and `lcAny` in the new code generator.
This commit is contained in:
Leonardo de Moura 2022-10-05 05:09:19 -07:00
parent 6288181656
commit ee59048bfb
2 changed files with 0 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Prelude.lean
View file

@ -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.

1
tests/lean/lcnfTypes.lean
View file

@ -1,7 +1,6 @@
import Lean
notation "◾" => lcErased
notation "⊤" => lcAny
open Lean Compiler LCNF Meta