Documentation

Lean.Data.EditDistance

def Lean.EditDistance.levenshtein (str1 str2 : String) (cutoff : 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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For