def Lean.EditDistance.levenshtein (str1 str2 : String) (cutoff : Nat) : Option Nat

Computes the Levenshtein distance between two strings, up to some cutoff.

If the return value is none, then the distance is certainly greater than the cutoff value, but a returned some does not necessarily indicate that the edit distance is less than or equal to the cutoff.