Commit 2023-08-29 12:49 46f6f340

View on Github →

feat: Estimator typeclass and implementation for Levenshtein distance (#6119)

Estimated changes

Modified Mathlib.lean

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

added structure LevenshteinEstimator'

added def LevenshteinEstimator

Created Mathlib/Order/Estimator.lean

added structure Estimator.fst

added def Estimator.fstInst

added def Estimator.improveUntil

added def Estimator.improveUntilAux

added theorem Estimator.improveUntilAux_spec

added theorem Estimator.improveUntil_spec