Documentation

Lake.Util.Name

First tries to convert a string into a legal name. If that fails, defaults to making it a simple name (e.g., Lean.Name.mkSimple).

Equations
Instances For
    @[inline]
    Equations
    • Lake.NameMap.empty = Lean.RBMap.empty
    Instances For
      instance Lake.instForInNameMapProdName_lake {m : Type u_1 → Type u_2} {α : Type} :
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • Lake.instCoeRBMapNameQuickCmpNameMap_lake = { coe := id }
      @[reducible, inline]
      abbrev Lake.OrdNameMap (α : Type u_1) :
      Type u_1
      Equations
      Instances For
        @[inline]
        Equations
        • Lake.OrdNameMap.empty = Lake.RBArray.empty
        Instances For
          @[inline]
          Equations
          Instances For
            @[reducible, inline]
            abbrev Lake.DNameMap (α : Lake.NameType u_1) :
            Type u_1
            Equations
            Instances For
              @[inline]
              Equations
              • Lake.DNameMap.empty = Lake.DRBMap.empty
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                • One or more equations did not get rendered due to their size.

                Name Helpers #

                @[simp]
                theorem Lake.Name.beq_false (m : Lake.Name) (n : Lake.Name) :
                (m == n) = false ¬m = n
                @[simp]
                theorem Lake.Name.isPrefixOf_self {n : Lake.Name} :
                n.isPrefixOf n = true
                @[simp]
                theorem Lake.Name.isPrefixOf_append {n : Lake.Name} {m : Lake.Name} :
                ¬n.hasMacroScopes = true¬m.hasMacroScopes = truen.isPrefixOf (n ++ m) = true
                @[simp]
                theorem Lake.Name.quickCmpAux_iff_eq {n : Lake.Name} {n' : Lake.Name} :
                n.quickCmpAux n' = Ordering.eq n = n'
                theorem Lake.Name.eq_of_quickCmp {n : Lake.Name} {n' : Lake.Name} :
                n.quickCmp n' = Ordering.eqn = n'
                Equations
                Instances For