Skip to content

Commit d1cdb34

Browse files
fgdoraisfgdorais
committed
chore: refactor Data.Nat.Bitwise
1 parent bf597c7 commit d1cdb34

File tree

2 files changed

+1
-1
lines changed

2 files changed

+1
-1
lines changed

‎Batteries/Data/Nat.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ module
22

33
public import Batteries.Data.Nat.Basic
44
public import Batteries.Data.Nat.Bisect
5-
public import Batteries.Data.Nat.Bitwise
5+
public import Batteries.Data.Nat.Bitwise.Lemmas
66
public import Batteries.Data.Nat.Gcd
77
public import Batteries.Data.Nat.Lemmas

Batteries/Data/Nat/Bitwise.lean renamed to Batteries/Data/Nat/Bitwise/Lemmas.lean

File renamed without changes.

0 commit comments

Comments
 (0)