Documentation

Lean.Data.Name

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