structure Lean.DeclarationRange : Type

Store position information for declarations.

• pos : Lean.Position
• charUtf16 : Nat

  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.

• endPos : Lean.Position
• endCharUtf16 : Nat

  See charUtf16.

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 = Lean.decEqDeclarationRange✝

instance Lean.instReprDeclarationRange : Repr Lean.DeclarationRange

Equations

• Lean.instReprDeclarationRange = { reprPrec := Lean.reprDeclarationRange✝ }

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 := Lean.reprDeclarationRanges✝ }

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 (Lake.NameMap Lean.DeclarationRanges)

opaque Lean.declRangeExt : Lean.MapDeclarationExtension Lean.DeclarationRanges

def Lean.addBuiltinDeclarationRanges (declName : Lake.Name) (declRanges : Lean.DeclarationRanges) : IO Unit

Equations

• Lean.addBuiltinDeclarationRanges declName declRanges = ST.Ref.modify Lean.builtinDeclRanges fun (x : Lake.NameMap Lean.DeclarationRanges) => x.insert declName declRanges

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

Equations

• Lean.addDeclarationRanges declName declRanges = Lean.modifyEnv fun (env : Lean.Environment) => Lean.declRangeExt.insert env declName declRanges

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

Equations

• Lean.findDeclarationRangesCore? declName = do let __do_lift ← Lean.getEnv pure (Lean.declRangeExt.find? __do_lift declName)

def Lean.findDeclarationRanges? {m : Type → Type} [Monad m] [Lean.MonadEnv m] [MonadLiftT BaseIO m] (declName : Lake.Name) : m (Option Lean.DeclarationRanges)

Equations

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