@[inline]

def Subarray.findSomeRev? {α : Type u} {β : Type v} (as : Subarray α) (p : α → Option β) : Option β

Equations

• as.findSomeRev? p = (as.findSomeRevM? fun (x : α) => pure (p x)).run

@[inline]

def Subarray.findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : α → m (Option β)) : m (Option β)

Equations

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

@[inline]

def Subarray.findM? {α : Type} {m : Type → Type w} [Monad m] (as : Subarray α) (p : α → m Bool) : m (Option α)

Equations

• as.findM? p = as.findSomeM? fun (a : α) => do let __do_lift ← p a pure (if __do_lift = true then some a else none)

@[inline]

def Subarray.find? {α : Type} (as : Subarray α) (p : α → Bool) : Option α

Equations

• as.find? p = (as.findM? fun (x : α) => pure (p x)).run

def Mathlib.Linter.Indentation.declarationLinter : IndentationLinter

docstring TODO. https://leanprover-community.github.io/contribute/style.html#structuring-definitions-and-theorems

Equations

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

def Mathlib.Linter.Indentation.passToChildren (childrenLinter : IndentationLinter := runLinterOn) : IndentationLinter

docstring TODO.

Equations

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

def Mathlib.Linter.Indentation.stringLinter : IndentationLinter

Equations

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

def Mathlib.Linter.Indentation.notAfterLineBreakLinter : IndentationLinter

Equations

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

def Mathlib.Linter.Indentation.additionalIndentationLinter (childrenLinter : IndentationLinter := runLinterOn) (additionalIndentation? : Option Nat := none) (strict : Bool := false) : IndentationLinter

docstring TODO.

Equations

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

def Mathlib.Linter.Indentation.strictAdditionalIndentationLinter (childrenLinter : IndentationLinter := runLinterOn) (additionalIndentation? : Option Nat := none) : IndentationLinter

Equations

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

def Mathlib.Linter.Indentation.aligningIndentationLinter (childrenLinter : IndentationLinter := runLinterOn) : IndentationLinter

Equations

• Mathlib.Linter.Indentation.aligningIndentationLinter childrenLinter = Mathlib.Linter.Indentation.additionalIndentationLinter childrenLinter (some 0) true

def Mathlib.Linter.Indentation.byLinter : IndentationLinter

Equations

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

def Mathlib.Linter.Indentation.termAppLinter : IndentationLinter

docstring TODO.

Equations

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

def Mathlib.Linter.Indentation.ignoringAdditionalIndentationLinter : IndentationLinter

Equations

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

def Mathlib.Linter.Indentation.nodeLinters : Lean.NameMap IndentationLinter

docstring TODO

Equations

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

def Mathlib.Linter.Indentation.atomLinters : Std.HashMap String IndentationLinter

Equations

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

def Mathlib.Linter.Indentation.brackets : Std.HashMap String (String × Nat)

from https://github.com/leanprover/vscode-lean4/blob/v0.0.209/vscode-lean4/language-configuration.json

Equations

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

def Mathlib.Linter.Indentation.bracketPairLinter (allowRightBracketDeeper : Bool := false) : IndentationLinter

Equations

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