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
          def Lean.Data.Trie.upsert {α : Type} (t : Trie α) (s : String) (f : Option αα) :
          Trie α

          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) :
              Trie α
              partial def Lean.Data.Trie.upsert.loop {α : Type} (s : String) (f : Option αα) :
              NatTrie αTrie α
              def Lean.Data.Trie.insert {α : Type} (t : Trie α) (s : String) (val : α) :
              Trie α

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

              Equations
                Instances For
                  def Lean.Data.Trie.find? {α : Type} (t : 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) :
                      NatTrie αOption α
                      def Lean.Data.Trie.values {α : Type} (t : Trie α) :

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

                      Equations
                        Instances For
                          partial def Lean.Data.Trie.values.go {α : Type} :
                          Trie αStateM (Array α) Unit
                          def Lean.Data.Trie.findPrefix {α : Type} (t : 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 : Trie α) (i : Nat) :
                              def Lean.Data.Trie.matchPrefix {α : Type} (s : String) (t : Trie α) (i : String.Pos) :

                              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) :
                                  Trie αNatOption αOption α
                                  Equations