Commit 2023-07-19 08:39 5dcd1aa4

View on Github →

chore: remove unneeded unsafe modifiers in ListM (#5989) These were left over from the era when ListM was unsafe.

Estimated changes

Modified Mathlib/Data/ListM/BestFirst.lean

added def bestFirstSearch

added def bestFirstSearchAux

Modified Mathlib/Data/ListM/DepthFirst.lean

added def depthFirstRemovingDuplicates