Documentation

Lean.Data.NameTrie

inductive Lean.NamePart :
Instances For
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Lean.NameTrie.insert {β : Type u_1} (t : Lean.NameTrie β) (n : Lake.Name) (b : β) :
        Equations
        Instances For
          Equations
          • Lean.NameTrie.empty = Lean.PrefixTree.empty
          Instances For
            Equations
            • Lean.instInhabitedNameTrie = { default := Lean.NameTrie.empty }
            Equations
            • Lean.instEmptyCollectionNameTrie = { emptyCollection := Lean.NameTrie.empty }
            def Lean.NameTrie.find? {β : Type u_1} (t : Lean.NameTrie β) (k : Lake.Name) :
            Equations
            Instances For
              @[inline]
              def Lean.NameTrie.foldMatchingM {m : Type u_1 → Type u_2} {β : Type u_3} {σ : Type u_1} [Monad m] (t : Lean.NameTrie β) (k : Lake.Name) (init : σ) (f : βσm σ) :
              m σ
              Equations
              Instances For
                @[inline]
                def Lean.NameTrie.foldM {m : Type u_1 → Type u_2} {β : Type u_3} {σ : Type u_1} [Monad m] (t : Lean.NameTrie β) (init : σ) (f : βσm σ) :
                m σ
                Equations
                Instances For
                  @[inline]
                  def Lean.NameTrie.forMatchingM {m : TypeType u_1} {β : Type u_2} [Monad m] (t : Lean.NameTrie β) (k : Lake.Name) (f : βm Unit) :
                  Equations
                  Instances For
                    @[inline]
                    def Lean.NameTrie.forM {m : TypeType u_1} {β : Type u_2} [Monad m] (t : Lean.NameTrie β) (f : βm Unit) :
                    Equations
                    Instances For