Skip to content

Commit 0bf7d0a

Browse files
committed
fix: public imports in Std
1 parent cc622b9 commit 0bf7d0a

File tree

1 file changed

+9
-8
lines changed

1 file changed

+9
-8
lines changed

src/Std.lean

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Sebastian Ullrich
55
-/
66
module
7+
78
prelude
8-
import Std.Data
9-
import Std.Do
10-
import Std.Sat
11-
import Std.Sync
12-
import Std.Time
13-
import Std.Tactic
14-
import Std.Internal
15-
import Std.Net
9+
public import Std.Data
10+
public import Std.Do
11+
public import Std.Sat
12+
public import Std.Sync
13+
public import Std.Time
14+
public import Std.Tactic
15+
public import Std.Internal
16+
public import Std.Net

0 commit comments

Comments
 (0)