Documentation

Lean.Data.FuzzyMatching

source
inductive Lean.FuzzyMatching.CharType :
Type

Represents the type of a single character.

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