Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Instances For
Instances For
Instances For
@[implemented_by Lean.Linter.MissingDocs.mkHandlerUnsafe]
def
Lean.Linter.MissingDocs.addHandler
(env : Lean.Environment)
(declName : Lean.Name)
(key : Lean.Name)
(h : Lean.Linter.MissingDocs.Handler)
:
Equations
- Lean.Linter.MissingDocs.addHandler env declName key h = Lean.Linter.MissingDocs.missingDocsExt.addEntry env (declName, key, h)
Instances For
Equations
- Lean.Linter.MissingDocs.getHandlers env = (Lean.Linter.MissingDocs.missingDocsExt.getState env).snd
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Linter.MissingDocs.addBuiltinHandler
(key : Lean.Name)
(h : Lean.Linter.MissingDocs.Handler)
:
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
Instances For
Equations
- Lean.Linter.MissingDocs.lint stx msg = Lean.Linter.logLint Lean.Linter.linter.missingDocs stx (Lean.toMessageData "missing doc string for " ++ Lean.toMessageData msg ++ Lean.toMessageData "")
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Linter.MissingDocs.lintStructField
(parent : Lean.Syntax)
(stx : Lean.Syntax)
(msg : String)
:
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.
Instances For
Equations
- Lean.Linter.MissingDocs.declModifiersPubNoDoc mods = (mods[2][0].getKind != `Lean.Parser.Command.private && mods[0].isNone && !Lean.Linter.MissingDocs.hasInheritDoc mods[1])
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
Equations
- Lean.Linter.MissingDocs.mkSimpleHandler name stx = if stx[0].isNone = true then Lean.Linter.MissingDocs.lintNamed stx[2] name else pure PUnit.unit
Instances For
Equations
- Lean.Linter.MissingDocs.checkSyntaxCat = Lean.Linter.MissingDocs.mkSimpleHandler "syntax category"
Instances For
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.
Instances For
Equations
- Lean.Linter.MissingDocs.checkClassAbbrev stx = if Lean.Linter.MissingDocs.declModifiersPubNoDoc stx[0] = true then Lean.Linter.MissingDocs.lintNamed stx[3] "class abbrev" else pure PUnit.unit
Instances For
Equations
- Lean.Linter.MissingDocs.checkSimpLike = Lean.Linter.MissingDocs.mkSimpleHandler "simp-like tactic"
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Linter.MissingDocs.handleMutual x stx = Array.forM Lean.Linter.MissingDocs.missingDocs.run stx[1].getArgs