Commit 2024-07-19 17:46 8b34afe5

View on Github →

chore: remove more easy autoImplicit (#14896)

Estimated changes

Modified Mathlib/Data/List/EditDistance/Bounds.lean

Modified Mathlib/Data/List/EditDistance/Estimator.lean

Modified Mathlib/Data/MLList/BestFirst.lean

modified structure BestFirstNode

Modified Mathlib/Data/MLList/Dedup.lean

Modified Mathlib/Data/MLList/DepthFirst.lean

Modified Mathlib/Data/MLList/IO.lean

Modified Mathlib/Data/MLList/Split.lean