Skip to content

Commit a1743c7

Browse files
committed
chore: shake Init
1 parent bebe1c5 commit a1743c7

File tree

493 files changed

+524
-504
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

493 files changed

+524
-504
lines changed

src/Init/BinderPredicates.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module
77

88
prelude
99
public import Init.NotationExtra
10+
import Init.Meta.Defs
1011

1112
public section
1213

src/Init/ByCases.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@ Authors: Leonardo de Moura, Mario Carneiro
66
module
77

88
prelude
9-
public import Init.Classical
9+
public import Init.Notation
10+
import Init.SimpLemmas
1011

1112
public section
1213

src/Init/Control/EState.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ module
77

88
prelude
99
public import Init.Control.State
10-
public import Init.Control.Except
1110
public import Init.Data.ToString.Basic
1211

1312
public section

src/Init/Control/Except.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ module
1010
prelude
1111
public import Init.Control.Basic
1212
public import Init.Control.Id
13-
public import Init.Coe
1413

1514
@[expose] public section
1615

src/Init/Control/Id.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ The identity Monad.
88
module
99

1010
prelude
11-
public import Init.Core
11+
public import Init.Prelude
1212

1313
public section
1414

src/Init/Control/Lawful/Basic.lean

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,7 @@ module
77

88
prelude
99
public import Init.Ext
10-
public import Init.SimpLemmas
11-
public import Init.Meta
10+
import Init.Grind.Attr
1211

1312
public section
1413

src/Init/Control/Lawful/Instances.lean

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,12 @@ module
77

88
prelude
99
public import Init.Control.Lawful.Basic
10-
public import Init.Control.Except
1110
import all Init.Control.Except
1211
public import Init.Control.Option
1312
import all Init.Control.Option
14-
public import Init.Control.State
1513
import all Init.Control.State
1614
public import Init.Control.StateRef
17-
public import Init.Ext
15+
import Init.Grind.Tactics
1816

1917
public section
2018

src/Init/Control/Lawful/Lemmas.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@ module
77

88
prelude
99
public import Init.Control.Lawful.Basic
10-
public import Init.RCases
1110
public import Init.ByCases
11+
public import Init.Classical
1212

1313
public section
1414

src/Init/Control/Lawful/MonadLift/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Quang Dao
66
module
77

88
prelude
9-
public import Init.Control.Basic
9+
public import Init.Notation
1010

1111
public section
1212

src/Init/Control/Lawful/MonadLift/Instances.lean

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,18 +8,17 @@ module
88
prelude
99
public import Init.Control.Option
1010
import all Init.Control.Option
11-
public import Init.Control.Except
1211
import all Init.Control.Except
1312
public import Init.Control.ExceptCps
1413
import all Init.Control.ExceptCps
1514
public import Init.Control.StateRef
1615
import all Init.Control.StateRef
1716
public import Init.Control.StateCps
1817
import all Init.Control.StateCps
19-
public import Init.Control.Id
2018
import all Init.Control.Id
2119
public import Init.Control.Lawful.MonadLift.Lemmas
2220
public import Init.Control.Lawful.Instances
21+
import Init.Grind.Tactics
2322

2423
public section
2524

0 commit comments

Comments
 (0)