Documentation

Lean.Data.FuzzyMatching

source
inductive Lean.FuzzyMatching.CharType :
Type

Represents the type of a single character.

source
def Lean.FuzzyMatching.charType (c : Char) :
Lean.FuzzyMatching.CharType
Equations
  • One or more equations did not get rendered due to their size.
source
inductive Lean.FuzzyMatching.CharRole :
Type

Represents the role of a character inside a word.

Instances For
source
instance Lean.FuzzyMatching.instInhabitedCharRole :
Inhabited Lean.FuzzyMatching.CharRole
Equations
source
@[inline]
def Lean.FuzzyMatching.charRole (prev? : Option Lean.FuzzyMatching.CharType) (curr : Lean.FuzzyMatching.CharType) (next? : Option Lean.FuzzyMatching.CharType) :
Lean.FuzzyMatching.CharRole
Equations
  • One or more equations did not get rendered due to their size.
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.FuzzyMatching.fuzzyMatchScoreWithThreshold? (pattern : String) (word : String) (threshold : optParam Float 0.1) :
Option Float
Equations
source
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.

Equations