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
  • One or more equations did not get rendered due to their size.
Instances For

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

    Instances For
      Equations
      • One or more equations did not get rendered due to their size.

      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
          • One or more equations did not get rendered due to their size.
          Equations
          • { docString? := docString?, visibility := Lean.Elab.Visibility.private, isNoncomputable := isNoncomputable, recKind := recKind, isUnsafe := isUnsafe, attrs := attrs }.isPrivate = true
          • x.isPrivate = false
          Instances For
            Equations
            • { docString? := docString?, visibility := Lean.Elab.Visibility.protected, isNoncomputable := isNoncomputable, recKind := recKind, isUnsafe := isUnsafe, attrs := attrs }.isProtected = true
            • x.isProtected = false
            Instances For
              Equations
              • { docString? := docString?, visibility := visibility, isNoncomputable := isNoncomputable, recKind := Lean.Elab.RecKind.partial, isUnsafe := isUnsafe, attrs := attrs }.isPartial = true
              • x.isPartial = false
              Instances For
                Equations
                • { docString? := docString?, visibility := visibility, isNoncomputable := isNoncomputable, recKind := Lean.Elab.RecKind.nonrec, isUnsafe := isUnsafe, attrs := attrs }.isNonrec = true
                • x.isNonrec = false
                Instances For

                  Adds attribute attr in modifiers

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Filters attributes using p

                    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.

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          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
                              Equations
                              • One or more equations did not get rendered due to their size.
                              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
                                • Lean.Elab.expandDeclIdCore declId = if declId.isIdent = true then (declId.getId, Lean.mkNullNode) else let id := declId[0].getId; let optUnivDeclStx := declId[1]; (id, optUnivDeclStx)
                                Instances For

                                  expandDeclId resulting type.

                                  • shortName : Lake.Name

                                    Short name for recursively referring to the declaration.

                                  • declName : Lake.Name

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

                                  • levelNames : List Lake.Name

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

                                  Instances For

                                    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
                                    • One or more equations did not get rendered due to their size.
                                    Instances For