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

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

Equations

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

@[inline, reducible]

abbrev Lean.Linter.MissingDocs.SimpleHandler : Type

Equations

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

@[inline, reducible]

abbrev Lean.Linter.MissingDocs.Handler : Type

Equations

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

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

Equations

• Lean.Linter.MissingDocs.SimpleHandler.toHandler h enabled stx = if enabled = true then h stx else pure ()

unsafe def Lean.Linter.MissingDocs.mkHandlerUnsafe (constName : Lake.Name) : Lean.ImportM Lean.Linter.MissingDocs.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 : Lake.Name) : Lean.ImportM Lean.Linter.MissingDocs.Handler

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

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

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

Equations

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

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

Equations

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

def Lean.Linter.MissingDocs.missingDocs : Lean.Linter

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Linter.MissingDocs.checkDecl : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkInit : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkNotation : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkMixfix : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkSyntax : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.mkSimpleHandler (name : String) : Lean.Linter.MissingDocs.SimpleHandler

Equations

• Lean.Linter.MissingDocs.mkSimpleHandler name stx = if Lean.Syntax.isNone stx[0] = true then Lean.Linter.MissingDocs.lintNamed stx[2] name else pure PUnit.unit

def Lean.Linter.MissingDocs.checkSyntaxAbbrev : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkSyntaxCat : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkMacro : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkElab : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkClassAbbrev : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkSimpLike : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkRegisterBuiltinOption : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.checkRegisterOption : Lean.Linter.MissingDocs.SimpleHandler

Equations

• Lean.Linter.MissingDocs.checkRegisterOption = Lean.Linter.MissingDocs.mkSimpleHandler "option"

def Lean.Linter.MissingDocs.checkRegisterSimpAttr : Lean.Linter.MissingDocs.SimpleHandler

Equations

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

def Lean.Linter.MissingDocs.handleIn : Lean.Linter.MissingDocs.Handler

Equations

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

def Lean.Linter.MissingDocs.handleMutual : Lean.Linter.MissingDocs.Handler

Equations

• Lean.Linter.MissingDocs.handleMutual x stx = Array.forM Lean.Linter.MissingDocs.missingDocs.run (Lean.Syntax.getArgs stx[1]) 0 (Array.size (Lean.Syntax.getArgs stx[1]))