Documentation

Lean.Data.Name

@[export lean_name_hash_exported]
Equations
    Instances For
      Equations
        Instances For
          Equations
            Instances For
              Equations
                Instances For
                  Equations
                    Instances For
                      Equations
                        Instances For
                          Equations
                            Instances For
                              Equations
                                Instances For
                                  Equations
                                    Instances For
                                      Equations
                                        Instances For
                                          Equations
                                            Instances For
                                              def Lean.Name.lt (x y : Name) :
                                              Equations
                                                Instances For
                                                  Equations
                                                    Instances For
                                                      def Lean.Name.quickCmp (n₁ n₂ : Name) :
                                                      Equations
                                                        Instances For
                                                          def Lean.Name.quickLt (n₁ n₂ : 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
                                                                    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
                                                                        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
                                                                            Instances For

                                                                              Check that a string begins with the given prefix, and then is only digits/'_'.

                                                                              Equations
                                                                                Instances For

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

                                                                                  Implementation-detail hypothesis names start with a double underscore.

                                                                                  Equations
                                                                                    Instances For
                                                                                      Equations
                                                                                        Instances For
                                                                                          Equations
                                                                                            Instances For
                                                                                              Equations
                                                                                                Instances For
                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      def Lean.Name.anyS (n : 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
                                                                                                        Instances For