Documentation

Lean.Elab.DeclModifiers

Ensure the environment does not contain a declaration with name declName. Recall that a private declaration cannot shadow a non-private one and vice-versa, although they internally have different names.

Equations
    Instances For

      Declaration visibility modifier. That is, whether a declaration is regular, protected or private.

      Instances For

        Whether a declaration is default, partial or nonrec.

        Instances For

          Flags and data added to declarations (eg docstrings, attributes, private, unsafe, partial, ...).

          Instances For
            Equations
              Instances For
                Equations
                  Instances For
                    Equations
                      Instances For

                        Adds attribute attr in modifiers

                        Equations
                          Instances For

                            Filters attributes using p

                            Equations
                              Instances For
                                def Lean.Elab.expandOptDocComment? {m : TypeType} [Monad m] [MonadError m] (optDocComment : Syntax) :

                                Retrieve doc string from stx of the form (docComment)?.

                                Equations
                                  Instances For
                                    def Lean.Elab.elabModifiers {m : TypeType} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (stx : TSyntax `Lean.Parser.Command.declModifiers) :

                                    Elaborate declaration modifiers (i.e., attributes, partial, private, protected, unsafe, noncomputable, doc string)

                                    Equations
                                      Instances For
                                        def Lean.Elab.applyVisibility {m : TypeType} [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (visibility : Visibility) (declName : Name) :

                                        Ensure the function has not already been declared, and apply the given visibility setting to declName. If private, return the updated name using our internal encoding for private names. If protected, register declName as protected in the environment.

                                        Equations
                                          Instances For
                                            Equations
                                              Instances For
                                                def Lean.Elab.mkDeclName {m : TypeType} [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (currNamespace : Name) (modifiers : Modifiers) (shortName : Name) :
                                                Equations
                                                  Instances For

                                                    declId is of the form

                                                    leading_parser ident >> optional (".{" >> sepBy1 ident ", " >> "}")
                                                    

                                                    but we also accept a single identifier to users to make macro writing more convenient .

                                                    Equations
                                                      Instances For

                                                        expandDeclId resulting type.

                                                        • shortName : Name

                                                          Short name for recursively referring to the declaration.

                                                        • declName : Name

                                                          Fully qualified name that will be used to name the declaration in the kernel.

                                                        • levelNames : List Name

                                                          Universe parameter names provided using the universe command and .{...} notation.

                                                        Instances For
                                                          def Lean.Elab.expandDeclId {m : TypeType} [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m] (currNamespace : Name) (currLevelNames : List Name) (declId : Syntax) (modifiers : Modifiers) :

                                                          Given a declaration identifier (e.g., ident (".{" ident,+ "}")?) that may contain explicit universe parameters

                                                          • Ensure the new universe parameters do not shadow universe parameters declared using universe command.
                                                          • Create the fully qualified named for the declaration using the current namespace, and given modifiers
                                                          • Create a short version for recursively referring to the declaration. Recall that the protected modifier affects the generation of the short name.

                                                          The result also contains the universe parameters provided using universe command, and the .{...} notation.

                                                          This commands also stores the doc string stored in modifiers.

                                                          Equations
                                                            Instances For