opaque Lean.Linter.linter.missingDocs : Lean.Option Bool

def Lean.Linter.getLinterMissingDocs (o : LinterOptions) : Bool

Equations

• Lean.Linter.getLinterMissingDocs o = Lean.Linter.getLinterValue Lean.Linter.linter.missingDocs o

@[reducible, inline]

abbrev Lean.Linter.MissingDocs.SimpleHandler : Type

Equations

• Lean.Linter.MissingDocs.SimpleHandler = (Lean.Syntax → Lean.Elab.Command.CommandElabM Unit)

@[reducible, inline]

abbrev Lean.Linter.MissingDocs.Handler : Type

Equations

• Lean.Linter.MissingDocs.Handler = (Bool → Lean.Linter.MissingDocs.SimpleHandler)

def Lean.Linter.MissingDocs.SimpleHandler.toHandler (h : SimpleHandler) : Handler

Equations

• h.toHandler enabled stx = if enabled = true then h stx else pure ()

unsafe def Lean.Linter.MissingDocs.mkHandlerUnsafe (constName : Name) : ImportM Handler

Equations

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

@[implemented_by Lean.Linter.MissingDocs.mkHandlerUnsafe]

opaque Lean.Linter.MissingDocs.mkHandler (constName : Name) : ImportM Handler

opaque Lean.Linter.MissingDocs.builtinHandlersRef : IO.Ref (NameMap Handler)

opaque Lean.Linter.MissingDocs.missingDocsExt : PersistentEnvExtension (Name × Name) (Name × Name × Handler) (List (Name × Name) × NameMap Handler)

def Lean.Linter.MissingDocs.addHandler (env : Environment) (declName key : Name) (h : Handler) : Environment

Equations

• Lean.Linter.MissingDocs.addHandler env declName key h = Lean.Linter.MissingDocs.missingDocsExt.addEntry env (declName, key, h)

def Lean.Linter.MissingDocs.getHandlers (env : Environment) : NameMap Handler

Equations

• Lean.Linter.MissingDocs.getHandlers env = (Lean.Linter.MissingDocs.missingDocsExt.getState env).snd

def Lean.Linter.MissingDocs.missingDocs : Linter

Equations

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

def Lean.Linter.MissingDocs.addBuiltinHandler (key : Name) (h : Handler) : IO Unit

Equations

• Lean.Linter.MissingDocs.addBuiltinHandler key h = ST.Ref.modify Lean.Linter.MissingDocs.builtinHandlersRef fun (x : Lean.NameMap Lean.Linter.MissingDocs.Handler) => x.insert key h

def Lean.Linter.MissingDocs.lint (stx : Syntax) (msg : String) : Elab.Command.CommandElabM Unit

Equations

• Lean.Linter.MissingDocs.lint stx msg = Lean.Linter.logLint Lean.Linter.linter.missingDocs stx (Lean.toMessageData "missing doc string for " ++ Lean.toMessageData msg)

def Lean.Linter.MissingDocs.lintEmpty (stx : Syntax) (msg : String) : Elab.Command.CommandElabM Unit

Equations

• Lean.Linter.MissingDocs.lintEmpty stx msg = Lean.Linter.logLint Lean.Linter.linter.missingDocs stx (Lean.toMessageData "empty doc string for " ++ Lean.toMessageData msg)

def Lean.Linter.MissingDocs.lintNamed (stx : Syntax) (msg : String) : Elab.Command.CommandElabM Unit

Equations

• Lean.Linter.MissingDocs.lintNamed stx msg = Lean.Linter.MissingDocs.lint stx (toString msg ++ toString " " ++ toString stx.getId)

def Lean.Linter.MissingDocs.lintEmptyNamed (stx : Syntax) (msg : String) : Elab.Command.CommandElabM Unit

Equations

• Lean.Linter.MissingDocs.lintEmptyNamed stx msg = Lean.Linter.MissingDocs.lintEmpty stx (toString msg ++ toString " " ++ toString stx.getId)

def Lean.Linter.MissingDocs.lintField (parent stx : Syntax) (msg : String) : Elab.Command.CommandElabM Unit

Equations

• Lean.Linter.MissingDocs.lintField parent stx msg = Lean.Linter.MissingDocs.lint stx (toString msg ++ toString " " ++ toString parent.getId ++ toString "." ++ toString stx.getId)

def Lean.Linter.MissingDocs.lintEmptyField (parent stx : Syntax) (msg : String) : Elab.Command.CommandElabM Unit

Equations

• Lean.Linter.MissingDocs.lintEmptyField parent stx msg = Lean.Linter.MissingDocs.lintEmpty stx (toString msg ++ toString " " ++ toString parent.getId ++ toString "." ++ toString stx.getId)

def Lean.Linter.MissingDocs.lintStructField (parent stx : Syntax) (msg : String) : Elab.Command.CommandElabM Unit

Equations

• Lean.Linter.MissingDocs.lintStructField parent stx msg = Lean.Linter.MissingDocs.lint stx (toString msg ++ toString " " ++ toString parent.getId ++ toString "." ++ toString stx.getId)

def Lean.Linter.MissingDocs.isMissingDoc (docOpt : Syntax) : Elab.Command.CommandElabM Bool

Equations

• Lean.Linter.MissingDocs.isMissingDoc docOpt = do let __do_lift ← Lean.Linter.MissingDocs.isEmptyDocString✝ docOpt pure (docOpt.isNone || __do_lift)

def Lean.Linter.MissingDocs.hasInheritDoc (attrs : Syntax) : Bool

Equations

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

def Lean.Linter.MissingDocs.hasTacticAlt (attrs : Syntax) : Bool

Equations

• Lean.Linter.MissingDocs.hasTacticAlt attrs = attrs[0][1].getSepArgs.any fun (attr : Lean.Syntax) => attr[1].isOfKind `Lean.Parser.Attr.tactic_alt

def Lean.Linter.MissingDocs.declModifiersDocStatus (mods : Syntax) : Elab.Command.CommandElabM (Option Bool)

Equations

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

def Lean.Linter.MissingDocs.declModifiersPubNoDoc (mods : Syntax) : Elab.Command.CommandElabM Bool

Equations

• Lean.Linter.MissingDocs.declModifiersPubNoDoc mods = do let __do_lift ← Lean.Linter.MissingDocs.declModifiersDocStatus mods pure __do_lift.isSome

def Lean.Linter.MissingDocs.lintDeclHead (k : SyntaxNodeKind) (id : Syntax) (isEmpty : Bool := false) : Elab.Command.CommandElabM Unit

Equations

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

def Lean.Linter.MissingDocs.checkDecl : SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkInit : SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkNotation : SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkMixfix : SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkSyntax : SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.mkSimpleHandler (name : String) (declNameStxIdx : Nat := 2) : SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkSyntaxAbbrev : SimpleHandler

Equations

• Lean.Linter.MissingDocs.checkSyntaxAbbrev = Lean.Linter.MissingDocs.mkSimpleHandler "syntax"

def Lean.Linter.MissingDocs.checkSyntaxCat : SimpleHandler

Equations

• Lean.Linter.MissingDocs.checkSyntaxCat = Lean.Linter.MissingDocs.mkSimpleHandler "syntax category"

def Lean.Linter.MissingDocs.checkMacro : SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkElab : SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkClassAbbrev : SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkSimpLike : SimpleHandler

Equations

• Lean.Linter.MissingDocs.checkSimpLike = Lean.Linter.MissingDocs.mkSimpleHandler "simp-like tactic"

def Lean.Linter.MissingDocs.checkRegisterBuiltinOption : SimpleHandler

Equations

• Lean.Linter.MissingDocs.checkRegisterBuiltinOption = Lean.Linter.MissingDocs.mkSimpleHandler "option" 3

def Lean.Linter.MissingDocs.checkRegisterOption : SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkRegisterSimpAttr : SimpleHandler

Equations

• Lean.Linter.MissingDocs.checkRegisterSimpAttr = Lean.Linter.MissingDocs.mkSimpleHandler "simp attr"

def Lean.Linter.MissingDocs.handleIn : Handler

Equations

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

def Lean.Linter.MissingDocs.handleMutual : Handler

Equations

• Lean.Linter.MissingDocs.handleMutual x✝ stx = Array.forM Lean.Linter.MissingDocs.missingDocs.run stx[1].getArgs