def Lean.findLineStart (s : String) (pos : String.Pos.Raw) : String.Pos.Raw

Return the beginning of the line contatining character pos.

Equations

• Lean.findLineStart s pos = ((Option.map (fun (x : s.Pos) => x.next!) ((s.pos! pos).revFind? '\n')).getD s.startPos).offset

def Lean.findIndentAndIsStart (s : String) (pos : String.Pos.Raw) : Nat × Bool

Return the indentation (number of leading spaces) of the line containing pos, and whether pos is the first non-whitespace character in the line.

Equations

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

def Lean.Position.getDeclsAfter (env : Environment) (pos : Position) (asyncMode : EnvExtension.AsyncMode := EnvExtension.AsyncMode.local) : Array Name

If pos is a Lean.Position, then pos.getDeclsAfter returns the array of names of declarations whose selection range begins in position at least pos. By using the selectionRange, which is usually smaller than the range, we err on the side of including declarations when possible.

By default, this only inspects the local branch of the environment. This is compatible with being used to find declarations from the current command in a linter, where we have already waited for async tasks/parallel branches to complete. Further, since the environment exposed to linters does not include constants added after the elaboration of the current command, it is safe to use this on the command's start position without picking up later declarations.

Equations

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

@[inline]

def String.Pos.Raw.getDeclsAfter (env : Lean.Environment) (map : Lean.FileMap) (pos : Raw) (asyncMode : Lean.EnvExtension.AsyncMode := Lean.EnvExtension.AsyncMode.local) : Array Lean.Name

If pos is a String.Pos.Raw, then pos.getDeclsAfter returns the array of names of declarations whose selection range begins in position at least pos. By using the selectionRange, which is usually smaller than the range, we err on the side of including declarations when possible.

By default, this is intended for use in linters, where only the current environment branch needs to be checked. See the docstring for Lean.Position.getDeclsAfter for details.

Equations

• String.Pos.Raw.getDeclsAfter env map pos asyncMode = Lean.Position.getDeclsAfter env (map.toPosition pos) asyncMode

def Lean.DeclarationRange.toSyntaxRange (map : FileMap) (range : DeclarationRange) : Syntax.Range

Converts a DeclarationRange to a Syntax.Range. This assumes that the DeclarationRange is sourced in the given FileMap.

Equations

• Lean.DeclarationRange.toSyntaxRange map range = { start := map.ofPosition range.pos, stop := map.ofPosition range.endPos }

def Lean.findDeclarationSyntaxRange? {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadFileMap m] (decl : Name) (fullRange : Bool := false) : m (Option Syntax.Range)

Yields the Syntax.Range for the declaration decl in the current file. If decl is not in the current file, yields none.

By default, this provides the "selection range", which is usually the declaration's identifier or e.g. the instance token for an unnamed instance. If fullRange is instead set to true, this returns the full declaration range (which includes modifiers, such as the docstring).

Equations

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

@[inline]

def Lean.withDeclRef? {α : Type} {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadFileMap m] [MonadRef m] (decl : Name) (x : m α) (fullRange : Bool := false) (canonical : Bool := true) : m α

Runs x with a synthetic ref that has position info locating the given decl if it is defined in the current file, or else runs x without modifying the ref. This is useful for logging on a declaration's name from within linters.

By default, this uses the "selection range" of the declaration, which is usually the declaration's identifier or e.g. the instance token for an unnamed instance. (This is also the place that receives hovers for the declaration.)

If fullRange is instead set to true, this uses the full declaration range, which includes the modifiers (such as the docstring, if there is one) and the body of the declaration.

canonical applies to the synthetic syntax generated for the ref; see Syntax.ofRange.

Equations

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