Documentation

Lean.Data.FuzzyMatching

source
inductive Lean.FuzzyMatching.CharType:
Type
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
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
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.2) :
Option Float
Equations
source
def Lean.FuzzyMatching.fuzzyMatch (pattern : String) (word : String) (threshold : optParam Float 0.2) :
Bool
Equations