Skip to content

Commit e330135

Browse files
committed
Clean
1 parent c26586c commit e330135

File tree

1 file changed

+0
-5
lines changed

1 file changed

+0
-5
lines changed

src/Init/Data/Ord/Basic.lean

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,11 +14,6 @@ import Init.ByCases
1414
import Init.Ext
1515
public import Init.PropLemmas
1616

17-
-- public import Init.Data.Array.Basic
18-
-- public import Init.Data.SInt.Basic
19-
-- public import Init.Data.Vector.Basic
20-
-- import all Init.Data.Vector.Basic
21-
2217
public section
2318

2419
/--

0 commit comments

Comments
 (0)