Skip to content

Commit b7d4b4a

Browse files
committed
Fix bootstrap issue
1 parent f3e8941 commit b7d4b4a

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Init/Data/Dyadic/Basic.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ prelude
99
public import Init.Data.Rat.Lemmas
1010
import Init.Data.Int.Bitwise.Lemmas
1111
import Init.Data.Int.DivMod.Lemmas
12+
import Init.Hints
1213

1314
/-!
1415
# The dyadic rationals

0 commit comments

Comments
 (0)