inductive Lean.FuzzyMatching.CharType : Type

• lower: Lean.FuzzyMatching.CharType
• upper: Lean.FuzzyMatching.CharType
• separator: Lean.FuzzyMatching.CharType

Represents the type of a single character.

def Lean.FuzzyMatching.charType (c : Char) : Lean.FuzzyMatching.CharType

inductive Lean.FuzzyMatching.CharRole : Type

• head: Lean.FuzzyMatching.CharRole
• tail: Lean.FuzzyMatching.CharRole
• separator: Lean.FuzzyMatching.CharRole

Represents the role of a character inside a word.

instance Lean.FuzzyMatching.instInhabitedCharRole : Inhabited Lean.FuzzyMatching.CharRole

@[inline]

def Lean.FuzzyMatching.charRole (prev? : Option Lean.FuzzyMatching.CharType) (curr : Lean.FuzzyMatching.CharType) (next? : Option Lean.FuzzyMatching.CharType) : Lean.FuzzyMatching.CharRole

def Lean.FuzzyMatching.fuzzyMatchScore? (pattern : String) (word : String) : Option Float

Match the given pattern with the given word using a fuzzy matching algorithm. The resulting scores are in the interval [0, 1] or none if no match was found.

def Lean.FuzzyMatching.fuzzyMatchScoreWithThreshold? (pattern : String) (word : String) (threshold : optParam Float 0.1) : Option Float

def Lean.FuzzyMatching.fuzzyMatch (pattern : String) (word : String) (threshold : optParam Float 0.2) : Bool

Match the given pattern with the given word using a fuzzy matching algorithm. Return false if no match was found or the found match received a score below the given threshold.