inductive Lean.FuzzyMatching.CharType : Type

Represents the type of a single character.

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

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

inductive Lean.FuzzyMatching.CharRole : Type

Represents the role of a character inside a word.

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

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 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

Equations

• Lean.FuzzyMatching.fuzzyMatchScoreWithThreshold? pattern word threshold = Option.filter (fun (x : Float) => decide (x > threshold)) (Lean.FuzzyMatching.fuzzyMatchScore? pattern word)

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.