fix: remove unintentionally-retained 'planned' label

leanprover · Feb 7, 2025 · cd0db8a · cd0db8a
1 parent b3c39de
commit cd0db8a
Showing 1 changed file with 0 additions and 6 deletions.
diff --git a/Manual/BasicTypes/Empty.lean b/Manual/BasicTypes/Empty.lean
@@ -17,12 +17,6 @@ set_option pp.rawOnError true
 tag := "empty"
 %%%
 
-:::planned 170
- * What is {lean}`Empty`?
- * Contrast with {lean}`Unit` and {lean}`False`
- * Definitional equality
-:::
-
 The empty type {name}`Empty` represents impossible values.
 It is an inductive type with no constructors whatsoever.