Documentation

Lean.PrivateName

Private name support. #

Suppose the user marks as declaration n as private. Then, we create the name: _private.<module_name>.0 ++ n. We say _private.<module_name>.0 is the "private prefix"

We assume that n is a valid user name and does not contain Name.num constructors. Thus, we can easily convert from private internal name to the user given name.

Equations
    Instances For
      def Lean.mkPrivateNameCore (mainModule n : Name) :
      Equations
        Instances For
          Equations
            Instances For
              @[export lean_is_private_name]
              Equations
                Instances For

                  Return true if n is of the form _private.<module_name>.0 See comment above.

                  Equations
                    Instances For
                      Equations
                        Instances For
                          @[export lean_private_to_user_name]
                          Equations
                            Instances For
                              Equations
                                Instances For
                                  @[export lean_private_prefix]
                                  Equations
                                    Instances For