def Mathlib.Linter.Indentation.ensureIndentationAt (treeInfo : SyntaxTreeInfo) (limit : Limitation) (checkAddition? : Option Bool := some true) (msgLtAtLeast : Option (Nat → Lean.MessageData) := some fun (x : Nat) => Lean.toMessageData "too few spaces, which should be at least " ++ Lean.toMessageData x ++ Lean.toMessageData "") (msgGtAtMost : Option (Nat → Lean.MessageData) := some fun (x : Nat) => Lean.toMessageData "too many spaces, which should be at most " ++ Lean.toMessageData x ++ Lean.toMessageData "") : LinterM Unit

docstring TODO

Equations

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

def Mathlib.Linter.Indentation.Limitation.forChildren (treeInfo : SyntaxTreeInfo) (limit : Limitation) (updateIndentation : Bool) : Lean.Elab.Command.CommandElabM Limitation

Equations

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

def Mathlib.Linter.Indentation.Limitation.forHead (treeInfo : SyntaxTreeInfo) (limit : Limitation) (updateIndentation : Bool) : Lean.Elab.Command.CommandElabM Limitation

Equations

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

def Mathlib.Linter.Indentation.ensureIndentationAtNode (treeInfo : SyntaxTreeInfo) (limit : Limitation) (checkAddition? updateIndentation? : Option Bool := none) (msgLtAtLeast : Option (Nat → Lean.MessageData) := some fun (x : Nat) => Lean.toMessageData "too few spaces, which should be at least " ++ Lean.toMessageData x ++ Lean.toMessageData "") (msgGtAtMost : Option (Nat → Lean.MessageData) := some fun (x : Nat) => Lean.toMessageData "too many spaces, which should be at most " ++ Lean.toMessageData x ++ Lean.toMessageData "") : LinterM (Limitation × Limitation)

docstring TODO

Equations

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

def Mathlib.Linter.Indentation.defaultLinter : IndentationLinter

Equations

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