Commit 2024-09-23 11:30 20d470bd

View on Github →

refactor: switch final use of Batteries.HashMap to Std.HashMap (#17042)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Std/Data/HashMap.lean

added def Std.HashMap.mapVal

Modified Mathlib/Tactic/Linarith/Datatypes.lean

Modified Mathlib/Tactic/Linarith/Frontend.lean

Modified Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean

modified def Linarith.CompSource.flatten

Modified Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean

modified def Linarith.SimplexAlgorithm.postprocess

Modified Mathlib/Tactic/Linarith/Verification.lean