Documentation

Lean.Data.FuzzyMatching

Represents the type of a single character.

Instances For
    Equations
      Instances For

        Represents the role of a character inside a word.

        Instances For
          @[inline]
          Equations
            Instances For

              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
                Instances For
                  def Lean.FuzzyMatching.fuzzyMatchScoreWithThreshold? (pattern word : String) (threshold : Float := 0.1) :
                  Equations
                    Instances For
                      def Lean.FuzzyMatching.fuzzyMatch (pattern word : String) (threshold : Float := 0.2) :

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