Documentation

Lean.DeclarationRange

structure Lean.DeclarationRange:

Type

pos : Lean.Position
A precomputed UTF-16 character field as in Lean.Lsp.Position. We need to store this because LSP clients want us to report the range in terms of UTF-16, but converting a Unicode codepoint stored in Lean.Position to UTF-16 requires loading and mapping the target source file, which is IO-heavy.
charUtf16 : Nat
endPos : Lean.Position
See charUtf16.
endCharUtf16 : Nat

instance Lean.instInhabitedDeclarationRange:

Inhabited Lean.DeclarationRange

Equations

Lean.instInhabitedDeclarationRange = { default := { pos := default, charUtf16 := default, endPos := default, endCharUtf16 := default } }

instance Lean.instDecidableEqDeclarationRange:

DecidableEq Lean.DeclarationRange

Equations

Lean.instDecidableEqDeclarationRange = [anonymous]

instance Lean.instReprDeclarationRange:

Repr Lean.DeclarationRange

Equations

Lean.instReprDeclarationRange = { reprPrec := [anonymous] }

instance Lean.instToExprDeclarationRange:

Lean.ToExpr Lean.DeclarationRange

Equations

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

structure Lean.DeclarationRanges:

Type

range : Lean.DeclarationRange
selectionRange : Lean.DeclarationRange

instance Lean.instInhabitedDeclarationRanges:

Inhabited Lean.DeclarationRanges

Equations

Lean.instInhabitedDeclarationRanges = { default := { range := default, selectionRange := default } }

instance Lean.instReprDeclarationRanges:

Repr Lean.DeclarationRanges

Equations

Lean.instReprDeclarationRanges = { reprPrec := [anonymous] }

instance Lean.instToExprDeclarationRanges:

Lean.ToExpr Lean.DeclarationRanges

Equations

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

opaque Lean.builtinDeclRanges:

IO.Ref (Lean.NameMap Lean.DeclarationRanges)

opaque Lean.declRangeExt:

Lean.MapDeclarationExtension Lean.DeclarationRanges

def Lean.addBuiltinDeclarationRanges (declName : Lean.Name) (declRanges : Lean.DeclarationRanges) :

Equations

Lean.addBuiltinDeclarationRanges declName declRanges = ST.Ref.modify Lean.builtinDeclRanges fun a => Lean.NameMap.insert a declName declRanges

def Lean.addDeclarationRanges {m : Type → Type} [inst : Lean.MonadEnv m] (declName : Lean.Name) (declRanges : Lean.DeclarationRanges) :

Equations

Lean.addDeclarationRanges declName declRanges = Lean.modifyEnv fun env => Lean.MapDeclarationExtension.insert Lean.declRangeExt env declName declRanges

def Lean.findDeclarationRangesCore? {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (declName : Lean.Name) :

m (Option Lean.DeclarationRanges)

Equations

Lean.findDeclarationRangesCore? declName = do let a ← Lean.getEnv pure (Lean.MapDeclarationExtension.find? Lean.declRangeExt a declName)

def Lean.findDeclarationRanges? {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : MonadLiftT IO m] (declName : Lean.Name) :

m (Option Lean.DeclarationRanges)

Equations

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