opaque Mathlib.Linter.linter.indentation : Lean.Option Bool

docstring TODO

structure Mathlib.Linter.Indentation.ChildrenHeadTail : Type

• head : SyntaxTreeInfo
• headToken : SyntaxTreeInfo
• tail : SyntaxTreeInfo
• tailToken : SyntaxTreeInfo

structure Mathlib.Linter.Indentation.ChildrenInfo : Type

docstring TODO

• children : Array SyntaxTreeInfo
• headTail? : Option ChildrenHeadTail
• outIdx : Nat

structure Mathlib.Linter.Indentation.ParentInfo : Type

docstring TODO

• parentIdx : Nat
• idxInChildren : Nat

instance Mathlib.Linter.Indentation.instInhabitedParentInfo : Inhabited ParentInfo

Equations

• Mathlib.Linter.Indentation.instInhabitedParentInfo = { default := { parentIdx := default, idxInChildren := default } }

instance Mathlib.Linter.Indentation.instInhabitedSyntaxTreeInfo : Inhabited SyntaxTreeInfo

Equations

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

structure Mathlib.Linter.Indentation.SyntaxTreeInfo : Type

docstring TODO

• stx : Lean.Syntax
• idx : Nat
• childrenInfo? : Option ChildrenInfo
• parentInfo? : Option ParentInfo
• prevTokenIdx? : Option Nat
• nextTokenIdx? : Option Nat

inductive Mathlib.Linter.Indentation.FlattenSyntaxTreeInfoElement : Type

docstring TODO

• leaf (info : SyntaxTreeInfo) : FlattenSyntaxTreeInfoElement
• into (info : SyntaxTreeInfo) : FlattenSyntaxTreeInfoElement
• out (info : SyntaxTreeInfo) : FlattenSyntaxTreeInfoElement

instance Mathlib.Linter.Indentation.instInhabitedFlattenSyntaxTreeInfoElement : Inhabited FlattenSyntaxTreeInfoElement

Equations

• Mathlib.Linter.Indentation.instInhabitedFlattenSyntaxTreeInfoElement = { default := Mathlib.Linter.Indentation.FlattenSyntaxTreeInfoElement.leaf default }

@[reducible, inline]

abbrev Mathlib.Linter.Indentation.FlattenSyntaxTreeInfo : Type

docstring TODO

Equations

• Mathlib.Linter.Indentation.FlattenSyntaxTreeInfo = Array Mathlib.Linter.Indentation.FlattenSyntaxTreeInfoElement

def Mathlib.Linter.Indentation.FlattenSyntaxTreeInfoElement.info : FlattenSyntaxTreeInfoElement → SyntaxTreeInfo

docstring TODO

Equations

• (Mathlib.Linter.Indentation.FlattenSyntaxTreeInfoElement.leaf info).info = info
• (Mathlib.Linter.Indentation.FlattenSyntaxTreeInfoElement.into info).info = info
• (Mathlib.Linter.Indentation.FlattenSyntaxTreeInfoElement.out info).info = info

def Mathlib.Linter.Indentation.SyntaxTreeInfo.children? (treeInfo : SyntaxTreeInfo) : Option (Array SyntaxTreeInfo)

docstring TODO

Equations

• treeInfo.children? = Option.map (fun (x : Mathlib.Linter.Indentation.ChildrenInfo) => x.children) treeInfo.childrenInfo?

def Mathlib.Linter.Indentation.SyntaxTreeInfo.isToken (treeInfo : SyntaxTreeInfo) : Bool

Equations

• treeInfo.isToken = treeInfo.childrenInfo?.isNone

def Mathlib.Linter.Indentation.SyntaxTreeInfo.headToken? (treeInfo : SyntaxTreeInfo) : Option SyntaxTreeInfo

Equations

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

def Mathlib.Linter.Indentation.SyntaxTreeInfo.headTokenIdx? (treeInfo : SyntaxTreeInfo) : Option Nat

Equations

• treeInfo.headTokenIdx? = Option.map (fun (x : Mathlib.Linter.Indentation.SyntaxTreeInfo) => x.idx) treeInfo.headToken?

def Mathlib.Linter.Indentation.SyntaxTreeInfo.tailToken? (treeInfo : SyntaxTreeInfo) : Option SyntaxTreeInfo

Equations

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

def Mathlib.Linter.Indentation.SyntaxTreeInfo.tailTokenIdx? (treeInfo : SyntaxTreeInfo) : Option Nat

Equations

• treeInfo.tailTokenIdx? = Option.map (fun (x : Mathlib.Linter.Indentation.SyntaxTreeInfo) => x.idx) treeInfo.tailToken?

def Mathlib.Linter.Indentation.FlattenSyntaxTreeInfoElement.nextTokenIdx? : FlattenSyntaxTreeInfoElement → Option Nat

Equations

• (Mathlib.Linter.Indentation.FlattenSyntaxTreeInfoElement.out i).nextTokenIdx? = i.nextTokenIdx?
• (Mathlib.Linter.Indentation.FlattenSyntaxTreeInfoElement.leaf i).nextTokenIdx? = i.nextTokenIdx?
• (Mathlib.Linter.Indentation.FlattenSyntaxTreeInfoElement.into i).nextTokenIdx? = (i.headTokenIdx? <|> i.nextTokenIdx?)

class Mathlib.Linter.Indentation.ForInTokens : Type

• subarray : Subarray FlattenSyntaxTreeInfoElement

def Mathlib.Linter.Indentation.forInTokens (subarray : Subarray FlattenSyntaxTreeInfoElement) : ForInTokens

Equations

• Mathlib.Linter.Indentation.forInTokens subarray = { subarray := subarray }

def Mathlib.Linter.Indentation.FlattenSyntaxTreeInfo.forInTokens (array : FlattenSyntaxTreeInfo) : ForInTokens

Equations

• array.forInTokens = { subarray := Array.toSubarray array }

instance Mathlib.Linter.Indentation.instForInForInTokensFlattenSyntaxTreeInfoElement {m : Type u_1 → Type u_2} : ForIn m ForInTokens FlattenSyntaxTreeInfoElement

Equations

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

@[specialize #[]]

partial def Mathlib.Linter.Indentation.instForInForInTokensFlattenSyntaxTreeInfoElement.loop {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (f : FlattenSyntaxTreeInfoElement → β → m (ForInStep β)) (stop : Nat) (array : Array FlattenSyntaxTreeInfoElement) (i : Nat) (state : β) : m β

def Mathlib.Linter.Indentation.ChildrenHeadTail.getInfo (headTail : ChildrenHeadTail) : Lean.SourceInfo

Equations

• headTail.getInfo = Lean.SourceInfo.synthetic headTail.head.stx.getPos?.get! headTail.tail.stx.getTailPos?.get!

def Mathlib.Linter.Indentation.ChildrenHeadTail.getHeadIdxInChildren (headTail : ChildrenHeadTail) : Nat

Equations

• headTail.getHeadIdxInChildren = headTail.head.parentInfo?.get!.idxInChildren

def Mathlib.Linter.Indentation.ChildrenHeadTail.getTailIdxInChildren (headTail : ChildrenHeadTail) : Nat

Equations

• headTail.getTailIdxInChildren = headTail.tail.parentInfo?.get!.idxInChildren

def Mathlib.Linter.Indentation.SyntaxTreeInfo.hasToken (treeInfo : SyntaxTreeInfo) : Bool

Equations

• treeInfo.hasToken = (treeInfo.isToken || treeInfo.childrenInfo?.elim false fun (x : Mathlib.Linter.Indentation.ChildrenInfo) => x.headTail?.isSome)

def Mathlib.Linter.Indentation.SyntaxTreeInfo.getInfo? (treeInfo : SyntaxTreeInfo) : Option Lean.SourceInfo

docstring TODO

Equations

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

def Mathlib.Linter.Indentation.SyntaxTreeInfo.getPos? (treeInfo : SyntaxTreeInfo) : Option String.Pos

docstring TODO

Equations

• treeInfo.getPos? = Option.map (fun (x : Lean.SourceInfo) => x.getPos?.get!) treeInfo.getInfo?

def Mathlib.Linter.Indentation.SyntaxTreeInfo.getTailPos? (treeInfo : SyntaxTreeInfo) : Option String.Pos

docstring TODO

Equations

• treeInfo.getTailPos? = Option.map (fun (x : Lean.SourceInfo) => x.getTailPos?.get!) treeInfo.getInfo?

def Mathlib.Linter.Indentation.SyntaxTreeInfo.getSrc? (treeInfo : SyntaxTreeInfo) : Option String

Equations

• treeInfo.getSrc? = Option.map (fun (x : Mathlib.Linter.Indentation.SyntaxTreeInfo) => x.stx.getInfo?.get!.getTrailing?.get!.str) treeInfo.headToken?

def Mathlib.Linter.Indentation.SyntaxTreeInfo.getSubstring? (treeInfo : SyntaxTreeInfo) : Option Substring

Equations

• treeInfo.getSubstring? = Option.map (fun (x : String.Pos) => { str := treeInfo.getSrc?.get!, startPos := x, stopPos := treeInfo.getTailPos?.get! }) treeInfo.getPos?

def Mathlib.Linter.Indentation.SyntaxTreeInfo.headTailOfChildren (children : Array SyntaxTreeInfo) : Option (Nat × Nat)

docstringTODO

Equations

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

partial def Mathlib.Linter.Indentation.SyntaxTreeInfo.ofSyntaxAux (stx : Lean.Syntax) (parentInfo : Option ParentInfo) : StateM (FlattenSyntaxTreeInfo × Option Nat) SyntaxTreeInfo

docstring TODO

partial def Mathlib.Linter.Indentation.SyntaxTreeInfo.updateNextTokenIdx (treeInfo : SyntaxTreeInfo) : StateM (FlattenSyntaxTreeInfo × Option Nat) SyntaxTreeInfo

docstring TODO

def Mathlib.Linter.Indentation.SyntaxTreeInfo.ofSyntax (stx : Lean.Syntax) : SyntaxTreeInfo × FlattenSyntaxTreeInfo

docstring TODO

Equations

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

def Mathlib.Linter.Indentation.indentationOfPos (str : String) (pos : String.Pos) : Option Nat

docstring TODO

Equations

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

def Mathlib.Linter.Indentation.indentationBeforePos (str : String) (pos : String.Pos) : Nat

docstring TODO

Equations

• Mathlib.Linter.Indentation.indentationBeforePos str pos = ({ str := str, startPos := str.findLineStart pos, stopPos := pos }.takeWhile fun (x : Char) => x == ' ').bsize

def Mathlib.Linter.Indentation.SyntaxTreeInfo.getIndentation? (treeInfo : SyntaxTreeInfo) : Option Nat

Equations

• treeInfo.getIndentation? = treeInfo.getPos?.bind fun (x : String.Pos) => Mathlib.Linter.Indentation.indentationOfPos treeInfo.getSrc?.get! x

def Mathlib.Linter.Indentation.categoriesContain {m : Type → Type} [Monad m] [Lean.MonadEnv m] (stx : Lean.Syntax) : m Bool

Equations

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

def Mathlib.Linter.Indentation.SyntaxTreeInfo.needUpdatingIndentation {m : Type → Type} [Monad m] [Lean.MonadEnv m] (treeInfo : SyntaxTreeInfo) : m Bool

Equations

• treeInfo.needUpdatingIndentation = Mathlib.Linter.Indentation.categoriesContain treeInfo.stx

instance Mathlib.Linter.Indentation.instToStringChildrenHeadTail : ToString ChildrenHeadTail

Equations

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

instance Mathlib.Linter.Indentation.instToStringParentInfo : ToString ParentInfo

Equations

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

instance Mathlib.Linter.Indentation.instToMessageDataSyntaxTreeInfo : Lean.ToMessageData SyntaxTreeInfo

Equations

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

partial def Mathlib.Linter.Indentation.instToMessageDataSyntaxTreeInfo.go (i : SyntaxTreeInfo) (n : Nat) : Id Lean.MessageData

structure Mathlib.Linter.Indentation.Limitation : Type

docstring TODO

• indentation : Nat
• additionalIndentation : Nat
• oneAdditionalIndentation : Nat
• isExactIndentation : Bool
• atMost : Option Nat

instance Mathlib.Linter.Indentation.instReprLimitation : Repr Limitation

Equations

• Mathlib.Linter.Indentation.instReprLimitation = { reprPrec := Mathlib.Linter.Indentation.reprLimitation✝ }

structure Mathlib.Linter.Indentation.IndentationError : Type

• msg : Lean.MessageData
• stx : Lean.Syntax

inductive Mathlib.Linter.Indentation.Result : Type

• nextLinter (limit : Limitation) : Result
• finished : Result

instance Mathlib.Linter.Indentation.instInhabitedResult : Inhabited Result

Equations

• Mathlib.Linter.Indentation.instInhabitedResult = { default := Mathlib.Linter.Indentation.Result.finished }

@[reducible, inline]

abbrev Mathlib.Linter.Indentation.LinterM (α : Type) : Type

Equations

• Mathlib.Linter.Indentation.LinterM = ReaderT (Mathlib.Linter.Indentation.FlattenSyntaxTreeInfo × String) (ExceptT Mathlib.Linter.Indentation.IndentationError Lean.Elab.Command.CommandElabM)

def Mathlib.Linter.Indentation.getFlatten : LinterM FlattenSyntaxTreeInfo

Equations

• Mathlib.Linter.Indentation.getFlatten = Prod.fst <$> read

def Mathlib.Linter.Indentation.getSrc : LinterM String

Equations

• Mathlib.Linter.Indentation.getSrc = Prod.snd <$> read

def Mathlib.Linter.Indentation.throwIndentationError (info : SyntaxTreeInfo) (msg : Lean.MessageData) (range : Option String.Range := Option.map (fun (p : String.Pos) => { start := info.getSrc?.get!.findLineStart p, stop := p }) info.getPos?) : LinterM Unit

docstring TODO

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Linter.Indentation.throwIndentationError info msg range = throwThe Mathlib.Linter.Indentation.IndentationError { msg := msg, stx := info.stx }

def Mathlib.Linter.Indentation.IndentationLinter : Type

docstring TODO

Equations

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

instance Mathlib.Linter.Indentation.instAndThenIndentationLinter : AndThen IndentationLinter

Equations

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

def Mathlib.Linter.Indentation.finishedLinter : IndentationLinter

Equations

• Mathlib.Linter.Indentation.finishedLinter x✝¹ x✝ = pure Mathlib.Linter.Indentation.Result.finished

structure Mathlib.Linter.Indentation.IndentationLinters : Type

• nodeLinters : Lean.NameMap IndentationLinter
• identLinters : Lean.NameMap IndentationLinter
• atomLinters : Std.HashMap String IndentationLinter
• linters : Array (Nat × IndentationLinter)

instance Mathlib.Linter.Indentation.instInhabitedIndentationLinters : Inhabited IndentationLinters

Equations

• Mathlib.Linter.Indentation.instInhabitedIndentationLinters = { default := { nodeLinters := default, identLinters := default, atomLinters := default, linters := default } }

instance Mathlib.Linter.Indentation.instEmptyCollectionIndentationLinters : EmptyCollection IndentationLinters

Equations

• Mathlib.Linter.Indentation.instEmptyCollectionIndentationLinters = { emptyCollection := { } }

def Mathlib.Linter.Indentation.Array.merge {α : Type u_1} (lt : α → α → Bool) (xs ys : Array α) : Array α

O(|xs| + |ys|). Merge arrays xs and ys. If the arrays are sorted according to lt, then the result is sorted as well. If two (or more) elements are equal according to lt, they are preserved.

From module Batteries.Data.Array.Merge.

Equations

• Mathlib.Linter.Indentation.Array.merge lt xs ys = Mathlib.Linter.Indentation.Array.merge.go lt xs ys (Array.mkEmpty (xs.size + ys.size)) 0 0

@[irreducible]

def Mathlib.Linter.Indentation.Array.merge.go {α : Type u_1} (lt : α → α → Bool) (xs ys acc : Array α) (i j : Nat) : Array α

Auxiliary definition for merge.

Equations

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

def Mathlib.Linter.Indentation.IndentationLinters.add (linters addedLinters : IndentationLinters) : IndentationLinters

Equations

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

opaque Mathlib.Linter.Indentation.indentationLinterRef : IO.Ref IndentationLinters

def Mathlib.Linter.Indentation.addIndentationLinters (linter : IndentationLinters) (ref : IO.Ref IndentationLinters := indentationLinterRef) : IO Unit

Equations

• Mathlib.Linter.Indentation.addIndentationLinters linter ref = ST.Ref.modify ref fun (x : Mathlib.Linter.Indentation.IndentationLinters) => x.add linter

def Mathlib.Linter.Indentation.runLinterOn (ref : IO.Ref IndentationLinters := indentationLinterRef) : IndentationLinter

Equations

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

@[reducible, inline]

abbrev Mathlib.Linter.Indentation.ensure (treeInfo : SyntaxTreeInfo) (limit : Limitation) (linter : IndentationLinter := runLinterOn) : LinterM Unit

Equations

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

def Mathlib.Linter.Indentation.markSourceCode (src : Substring) (info? : Option Lean.SourceInfo) (msg : Lean.MessageData) (afterError : Nat := 3) : Lean.Elab.Command.CommandElabM Lean.MessageData

Equations

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

def Mathlib.Linter.Indentation.indentationLinter : Lean.Linter

docstring TODO

Equations

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