inductive Lean.FuzzyMatching.CharType : Type

Represents the type of a single character.

• lower : CharType
• upper : CharType
• separator : CharType

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

inductive Lean.FuzzyMatching.CharRole : Type

Represents the role of a character inside a word.

• head : CharRole
• tail : CharRole
• separator : CharRole

def Lean.FuzzyMatching.instInhabitedCharRole.default : CharRole

@[implicit_reducible]

instance Lean.FuzzyMatching.instInhabitedCharRole : Inhabited CharRole

@[inline]

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

def Lean.FuzzyMatching.fuzzyMatchScore? (pattern 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 word : String) (threshold : Float := 0.1) : Option Float

def Lean.FuzzyMatching.fuzzyMatch (pattern word : String) (threshold : 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.