Documentation

Lean.Data.Trie

inductive Lean.Data.Trie (α : Type) :

A Trie is a key-value store where the keys are of type String, and the internal structure is a tree that branches on the bytes of the string.

Instances For

    The empty Trie

    Equations
    Instances For
      Equations
      • Lean.Data.Trie.instEmptyCollection = { emptyCollection := Lean.Data.Trie.empty }
      Equations
      • Lean.Data.Trie.instInhabited = { default := Lean.Data.Trie.empty }
      def Lean.Data.Trie.upsert {α : Type} (t : Lean.Data.Trie α) (s : String) (f : Option αα) :

      Insert or update the value at a the given key s.

      Equations
      Instances For
        partial def Lean.Data.Trie.upsert.insertEmpty {α : Type} (s : String) (f : Option αα) (i : Nat) :
        partial def Lean.Data.Trie.upsert.loop {α : Type} (s : String) (f : Option αα) :
        def Lean.Data.Trie.insert {α : Type} (t : Lean.Data.Trie α) (s : String) (val : α) :

        Inserts a value at a the given key s, overriding an existing value if present.

        Equations
        • t.insert s val = t.upsert s fun (x : Option α) => val
        Instances For
          def Lean.Data.Trie.find? {α : Type} (t : Lean.Data.Trie α) (s : String) :

          Looks up a value at the given key s.

          Equations
          Instances For
            partial def Lean.Data.Trie.find?.loop {α : Type} (s : String) :
            NatLean.Data.Trie αOption α

            Returns an Array of all values in the trie, in no particular order.

            Equations
            Instances For
              def Lean.Data.Trie.findPrefix {α : Type} (t : Lean.Data.Trie α) (pre : String) :

              Returns all values whose key have the given string pre as a prefix, in no particular order.

              Equations
              Instances For
                partial def Lean.Data.Trie.findPrefix.go {α : Type} (pre : String) (t : Lean.Data.Trie α) (i : Nat) :

                Find the longest key in the trie that is contained in the given string s at position i, and return the associated value.

                Equations
                Instances For
                  partial def Lean.Data.Trie.matchPrefix.loop {α : Type} (s : String) :
                  Lean.Data.Trie αNatOption αOption α
                  Equations