Documentation

Lean.Data.PrefixTree

inductive Lean.PrefixTreeNode (α : Type u) (β : Type v) :
Type (max u v)
Instances For
    Equations
    def Lean.PrefixTreeNode.empty {α : Type u_1} {β : Type u_2} :
    Equations
    Instances For
      @[specialize #[]]
      def Lean.PrefixTreeNode.insert {α : Type u_1} {β : Type u_2} (t : Lean.PrefixTreeNode α β) (cmp : ααOrdering) (k : List α) (val : β) :
      Equations
      Instances For
        partial def Lean.PrefixTreeNode.insert.insertEmpty {α : Type u_1} {β : Type u_2} (val : β) (k : List α) :
        partial def Lean.PrefixTreeNode.insert.loop {α : Type u_1} {β : Type u_2} (cmp : ααOrdering) (val : β) :
        @[specialize #[]]
        def Lean.PrefixTreeNode.find? {α : Type u_1} {β : Type u_2} (t : Lean.PrefixTreeNode α β) (cmp : ααOrdering) (k : List α) :
        Equations
        Instances For
          partial def Lean.PrefixTreeNode.find?.loop {α : Type u_1} {β : Type u_2} (cmp : ααOrdering) :
          Lean.PrefixTreeNode α βList αOption β
          @[specialize #[]]
          def Lean.PrefixTreeNode.foldMatchingM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {σ : Type u_1} [Monad m] (t : Lean.PrefixTreeNode α β) (cmp : ααOrdering) (k : List α) (init : σ) (f : βσm σ) :
          m σ
          Equations
          Instances For
            partial def Lean.PrefixTreeNode.foldMatchingM.fold {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {σ : Type u_1} [Monad m] (f : βσm σ) :
            Lean.PrefixTreeNode α βσm σ
            partial def Lean.PrefixTreeNode.foldMatchingM.find {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {σ : Type u_1} [Monad m] (cmp : ααOrdering) (init : σ) (f : βσm σ) :
            List αLean.PrefixTreeNode α βσm σ
            inductive Lean.PrefixTreeNode.WellFormed {α : Type u_1} (cmp : ααOrdering) {β : Type u_2} :
            Instances For
              def Lean.PrefixTree (α : Type u) (β : Type v) (cmp : ααOrdering) :
              Type (max u v)
              Equations
              Instances For
                def Lean.PrefixTree.empty {α : Type u_1} {β : Type u_2} {p : ααOrdering} :
                Equations
                • Lean.PrefixTree.empty = Lean.PrefixTreeNode.empty,
                Instances For
                  instance Lean.instInhabitedPrefixTree {α : Type u_1} {β : Type u_2} {p : ααOrdering} :
                  Equations
                  • Lean.instInhabitedPrefixTree = { default := Lean.PrefixTree.empty }
                  instance Lean.instEmptyCollectionPrefixTree {α : Type u_1} {β : Type u_2} {p : ααOrdering} :
                  Equations
                  • Lean.instEmptyCollectionPrefixTree = { emptyCollection := Lean.PrefixTree.empty }
                  @[inline]
                  def Lean.PrefixTree.insert {α : Type u_1} {β : Type u_2} {p : ααOrdering} (t : Lean.PrefixTree α β p) (k : List α) (v : β) :
                  Equations
                  • t.insert k v = t.val.insert p k v,
                  Instances For
                    @[inline]
                    def Lean.PrefixTree.find? {α : Type u_1} {β : Type u_2} {p : ααOrdering} (t : Lean.PrefixTree α β p) (k : List α) :
                    Equations
                    • t.find? k = t.val.find? p k
                    Instances For
                      @[inline]
                      def Lean.PrefixTree.foldMatchingM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {p : ααOrdering} {σ : Type u_1} [Monad m] (t : Lean.PrefixTree α β p) (k : List α) (init : σ) (f : βσm σ) :
                      m σ
                      Equations
                      • t.foldMatchingM k init f = t.val.foldMatchingM p k init f
                      Instances For
                        @[inline]
                        def Lean.PrefixTree.foldM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {p : ααOrdering} {σ : Type u_1} [Monad m] (t : Lean.PrefixTree α β p) (init : σ) (f : βσm σ) :
                        m σ
                        Equations
                        • t.foldM init f = t.foldMatchingM [] init f
                        Instances For
                          @[inline]
                          def Lean.PrefixTree.forMatchingM {m : TypeType u_1} {α : Type u_2} {β : Type u_3} {p : ααOrdering} [Monad m] (t : Lean.PrefixTree α β p) (k : List α) (f : βm Unit) :
                          Equations
                          • t.forMatchingM k f = t.val.foldMatchingM p k () fun (b : β) (x : Unit) => f b
                          Instances For
                            @[inline]
                            def Lean.PrefixTree.forM {m : TypeType u_1} {α : Type u_2} {β : Type u_3} {p : ααOrdering} [Monad m] (t : Lean.PrefixTree α β p) (f : βm Unit) :
                            Equations
                            • t.forM f = t.forMatchingM [] f
                            Instances For