Documentation

Lean.Data.Name

@[export lean_name_hash_exported]
Equations
Instances For
    Equations
    Instances For
      Equations
      • x.getString! = match x with | pre.str s => s | x => panicWithPosWithDecl "Lean.Data.Name" "Lean.Name.getString!" 22 15 "unreachable code has been reached"
      Instances For
        Equations
        Instances For
          Equations
          Instances For
            Equations
            Instances For
              Equations
              • n.components = n.componentsRev.reverse
              Instances For
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    • Lean.Name.anonymous.isSuffixOf x = true
                    • (p₁.str s₁).isSuffixOf (p₂.str s₂) = (s₁ == s₂ && p₁.isSuffixOf p₂)
                    • (p₁.num n₁).isSuffixOf (p₂.num n₂) = (n₁ == n₂ && p₁.isSuffixOf p₂)
                    • x✝.isSuffixOf x = false
                    Instances For
                      Equations
                      Instances For
                        Equations
                        Instances For
                          Equations
                          Instances For
                            Equations
                            • n₁.quickCmp n₂ = match compare n₁.hash n₂.hash with | Ordering.eq => n₁.quickCmpAux n₂ | ord => ord
                            Instances For
                              def Lean.Name.quickLt (n₁ : Lake.Name) (n₂ : Lake.Name) :
                              Equations
                              Instances For

                                Returns true if the name has any numeric components.

                                Equations
                                Instances For

                                  The frontend does not allow user declarations to start with _ in any of its parts. We use name parts starting with _ internally to create auxiliary names (e.g., _private).

                                  Equations
                                  • (p.str s).isInternal = (s.get 0 == '_' || p.isInternal)
                                  • (p.num i).isInternal = p.isInternal
                                  • x.isInternal = false
                                  Instances For

                                    The frontend does not allow user declarations to start with _ in any of its parts. We use name parts starting with _ internally to create auxiliary names (e.g., _private).

                                    This function checks if any component of the name starts with _, or is numeric.

                                    Equations
                                    • (p.str s).isInternalOrNum = (s.get 0 == '_' || p.isInternalOrNum)
                                    • (p.num i).isInternalOrNum = true
                                    • x.isInternalOrNum = false
                                    Instances For

                                      Returns true if this a part of name that is internal or dynamically generated so that it may easily be changed.

                                      Generally, user code should not explicitly use internal names.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        Check that a string begins with the given prefix, and then is only digit characters.

                                        Equations
                                        Instances For

                                          Checks whether the name is an implementation-detail hypothesis name.

                                          Implementation-detail hypothesis names start with a double underscore.

                                          Equations
                                          • (Lean.Name.anonymous.str s).isImplementationDetail = s.startsWith "__"
                                          • (p.num i).isImplementationDetail = p.isImplementationDetail
                                          • (p.str str).isImplementationDetail = p.isImplementationDetail
                                          • Lean.Name.anonymous.isImplementationDetail = false
                                          Instances For
                                            Equations
                                            Instances For
                                              Equations
                                              Instances For
                                                Equations
                                                • x.isStr = match x with | pre.str str => true | x => false
                                                Instances For
                                                  Equations
                                                  • x.isNum = match x with | pre.num i => true | x => false
                                                  Instances For
                                                    def Lean.Name.anyS (n : Lake.Name) (f : StringBool) :

                                                    Return true if n contains a string part s that satisfies f.

                                                    Examples:

                                                    #eval (`foo.bla).anyS (·.startsWith "fo") -- true
                                                    #eval (`foo.bla).anyS (·.startsWith "boo") -- false
                                                    
                                                    Equations
                                                    • (p.str s).anyS f = (f s || p.anyS f)
                                                    • (p.num i).anyS f = p.anyS f
                                                    • n.anyS f = false
                                                    Instances For