Skip to content

Commit cd0db8a

Browse files
fix: remove unintentionally-retained 'planned' label
1 parent b3c39de commit cd0db8a

File tree

1 file changed

+0
-6
lines changed

1 file changed

+0
-6
lines changed

Manual/BasicTypes/Empty.lean

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -17,12 +17,6 @@ set_option pp.rawOnError true
1717
tag := "empty"
1818
%%%
1919

20-
:::planned 170
21-
* What is {lean}`Empty`?
22-
* Contrast with {lean}`Unit` and {lean}`False`
23-
* Definitional equality
24-
:::
25-
2620
The empty type {name}`Empty` represents impossible values.
2721
It is an inductive type with no constructors whatsoever.
2822

0 commit comments

Comments
 (0)