Skip to content

Commit 3a6fc3c

Browse files
JovanGerbReemMelamed
authored andcommitted
chore: adaptations for Aesop import reduction (leanprover-community#40217)
This PR adds an import, so that mathlib can adapt to the changes in leanprover-community/aesop#330. Bumping the aesop version to that PR improves mathlib's instructions by 0.15%: this is for a future PR.
1 parent 04c4aa1 commit 3a6fc3c

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

Mathlib/Tactic/Order/ToInt.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ public import Batteries.Tactic.GeneralizeProofs
1010
public import Mathlib.Tactic.Order.CollectFacts
1111
public meta import Mathlib.Util.AtomM
1212
public meta import Mathlib.Util.Qq
13+
public meta import Std.Data.HashMap.AdditionalOperations
1314

1415
/-!
1516
# Translating linear orders to ℤ

0 commit comments

Comments
 (0)