Documentation

Lean.Linter.MissingDocs

source
opaque Lean.Linter.linter.missingDocs :
Lean.Option Bool
source
def Lean.Linter.getLinterMissingDocs (o : LinterOptions) :
Bool
Instances For
    source
    @[reducible, inline]
    abbrev Lean.Linter.MissingDocs.SimpleHandler :
    Type
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Linter.MissingDocs.Handler :
      Type
      Instances For
        source
        def Lean.Linter.MissingDocs.SimpleHandler.toHandler (h : SimpleHandler) :
        Handler
        Instances For
          source
          unsafe def Lean.Linter.MissingDocs.mkHandlerUnsafe (constName : Name) :
          ImportM Handler
          Instances For
            source
            @[implemented_by Lean.Linter.MissingDocs.mkHandlerUnsafe]
            opaque Lean.Linter.MissingDocs.mkHandler (constName : Name) :
            ImportM Handler
            source
            opaque Lean.Linter.MissingDocs.builtinHandlersRef :
            IO.Ref (NameMap Handler)
            source
            opaque Lean.Linter.MissingDocs.missingDocsExt :
            PersistentEnvExtension (Name × Name) (Name × Name × Handler) (List (Name × Name) × NameMap Handler)
            source
            def Lean.Linter.MissingDocs.addHandler (env : Environment) (declName key : Name) (h : Handler) :
            Environment
            Instances For
              source
              def Lean.Linter.MissingDocs.getHandlers (env : Environment) :
              NameMap Handler
              Instances For
                source
                def Lean.Linter.MissingDocs.missingDocs :
                Linter
                Instances For
                  source
                  def Lean.Linter.MissingDocs.addBuiltinHandler (key : Name) (h : Handler) :
                  IO Unit
                  Instances For
                    source
                    def Lean.Linter.MissingDocs.lint (stx : Syntax) (msg : String) :
                    Elab.Command.CommandElabM Unit
                    Instances For
                      source
                      def Lean.Linter.MissingDocs.lintNamed (stx : Syntax) (msg : String) :
                      Elab.Command.CommandElabM Unit
                      Instances For
                        source
                        def Lean.Linter.MissingDocs.lintField (parent stx : Syntax) (msg : String) :
                        Elab.Command.CommandElabM Unit
                        Instances For
                          source
                          def Lean.Linter.MissingDocs.lintStructField (parent stx : Syntax) (msg : String) :
                          Elab.Command.CommandElabM Unit
                          Instances For
                            source
                            def Lean.Linter.MissingDocs.hasInheritDoc (attrs : Syntax) :
                            Bool
                            Instances For
                              source
                              def Lean.Linter.MissingDocs.hasTacticAlt (attrs : Syntax) :
                              Bool
                              Instances For
                                source
                                def Lean.Linter.MissingDocs.declModifiersPubNoDoc (mods : Syntax) :
                                Elab.Command.CommandElabM Bool
                                Instances For
                                  source
                                  def Lean.Linter.MissingDocs.lintDeclHead (k : SyntaxNodeKind) (id : Syntax) :
                                  Elab.Command.CommandElabM Unit
                                  Instances For
                                    source
                                    def Lean.Linter.MissingDocs.checkDecl :
                                    SimpleHandler
                                    Instances For
                                      source
                                      def Lean.Linter.MissingDocs.checkInit :
                                      SimpleHandler
                                      Instances For
                                        source
                                        def Lean.Linter.MissingDocs.checkNotation :
                                        SimpleHandler
                                        Instances For
                                          source
                                          def Lean.Linter.MissingDocs.checkMixfix :
                                          SimpleHandler
                                          Instances For
                                            source
                                            def Lean.Linter.MissingDocs.checkSyntax :
                                            SimpleHandler
                                            Instances For
                                              source
                                              def Lean.Linter.MissingDocs.mkSimpleHandler (name : String) (declNameStxIdx : Nat := 2) :
                                              SimpleHandler
                                              Instances For
                                                source
                                                def Lean.Linter.MissingDocs.checkSyntaxAbbrev :
                                                SimpleHandler
                                                Instances For
                                                  source
                                                  def Lean.Linter.MissingDocs.checkSyntaxCat :
                                                  SimpleHandler
                                                  Instances For
                                                    source
                                                    def Lean.Linter.MissingDocs.checkMacro :
                                                    SimpleHandler
                                                    Instances For
                                                      source
                                                      def Lean.Linter.MissingDocs.checkElab :
                                                      SimpleHandler
                                                      Instances For
                                                        source
                                                        def Lean.Linter.MissingDocs.checkClassAbbrev :
                                                        SimpleHandler
                                                        Instances For
                                                          source
                                                          def Lean.Linter.MissingDocs.checkSimpLike :
                                                          SimpleHandler
                                                          Instances For
                                                            source
                                                            def Lean.Linter.MissingDocs.checkRegisterBuiltinOption :
                                                            SimpleHandler
                                                            Instances For
                                                              source
                                                              def Lean.Linter.MissingDocs.checkRegisterOption :
                                                              SimpleHandler
                                                              Instances For
                                                                source
                                                                def Lean.Linter.MissingDocs.checkRegisterSimpAttr :
                                                                SimpleHandler
                                                                Instances For
                                                                  source
                                                                  def Lean.Linter.MissingDocs.handleIn :
                                                                  Handler
                                                                  Instances For
                                                                    source
                                                                    def Lean.Linter.MissingDocs.handleMutual :
                                                                    Handler
                                                                    Instances For