Documentation

Lean.Modifiers

@[export lean_add_protected]
Equations
Instances For
    @[export lean_is_protected]
    Equations
    Instances For

      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
        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
              @[export lean_private_to_user_name]
              Equations
              Instances For
                @[export lean_private_prefix]
                Equations
                Instances For