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

Equations

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

inductive Lean.FuzzyMatching.CharRole : Type

Represents the role of a character inside a word.

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

Instances For

• Lean.FuzzyMatching.instInhabitedCharRole

instance Lean.FuzzyMatching.instInhabitedCharRole : Inhabited CharRole

Equations

• Lean.FuzzyMatching.instInhabitedCharRole = { default := Lean.FuzzyMatching.CharRole.head }

@[inline]

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

Equations

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

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.

Equations

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

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.

Equations

• Lean.FuzzyMatching.fuzzyMatch pattern word threshold = (Lean.FuzzyMatching.fuzzyMatchScoreWithThreshold? pattern word threshold).isSome