Commit 2023-08-16 04:08 979bb0f9

View on Github →

feat: computation of Levenshtein edit distance (#6117) Subsequent PRs will prove properties of this definition, and implement the rw_search tactic using it.

Estimated changes

Modified Mathlib.lean

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

added structure Levenshtein.Cost

added def Levenshtein.defaultCost

added def Levenshtein.impl

added theorem Levenshtein.impl_cons

added theorem Levenshtein.impl_cons_fst_zero

added theorem Levenshtein.impl_length

added theorem List.eq_of_length_one

added def levenshtein

added theorem levenshtein_cons_cons

added theorem levenshtein_cons_nil

added theorem levenshtein_nil_cons

added theorem levenshtein_nil_nil

added def suffixLevenshtein

added theorem suffixLevenshtein_cons_cons_fst_get_zero

added theorem suffixLevenshtein_cons₁

added theorem suffixLevenshtein_cons₁_aux

added theorem suffixLevenshtein_cons₁_fst

added theorem suffixLevenshtein_cons₂

added theorem suffixLevenshtein_eq

added theorem suffixLevenshtein_eq_tails_map

added theorem suffixLevenshtein_length

added theorem suffixLevenshtein_nil'

added theorem suffixLevenshtein_nil_nil