source
inductive Lean.FuzzyMatching.CharType :
Type

Represents the type of a single character.

- lower : CharType
- upper : CharType
- separator : CharType

Instances For

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

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

Instances For

source
inductive Lean.FuzzyMatching.CharRole :
Type

Represents the role of a character inside a word.

- head : CharRole
- tail : CharRole
- separator : CharRole

Instances For

source
def Lean.FuzzyMatching.instInhabitedCharRole.default :
CharRole
Equations

- Lean.FuzzyMatching.instInhabitedCharRole.default = Lean.FuzzyMatching.CharRole.head

Instances For

source
instance Lean.FuzzyMatching.instInhabitedCharRole :
Inhabited CharRole
Equations

- Lean.FuzzyMatching.instInhabitedCharRole = { default := Lean.FuzzyMatching.instInhabitedCharRole.default }

source
@[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.

Instances For

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

Instances For

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

Instances For

source
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

Instances For