Data types for declaration ranges

The environment extension for declaration ranges is in Lean.DeclarationRange.

structure Lean.DeclarationRange : Type

Store position information for declarations.

• pos : 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 : Position
• endCharUtf16 : Nat

  See charUtf16.

instance Lean.instInhabitedDeclarationRange : Inhabited DeclarationRange

instance Lean.instDecidableEqDeclarationRange : DecidableEq DeclarationRange

instance Lean.instReprDeclarationRange : Repr DeclarationRange

instance Lean.instToExprDeclarationRange : ToExpr DeclarationRange

structure Lean.DeclarationRanges : Type

• range : DeclarationRange
• selectionRange : DeclarationRange

instance Lean.instInhabitedDeclarationRanges : Inhabited DeclarationRanges

instance Lean.instReprDeclarationRanges : Repr DeclarationRanges

instance Lean.instToExprDeclarationRanges : ToExpr DeclarationRanges

structure Lean.DeclarationLocation : Type

A declaration location is a declaration range along with the name of the module the declaration resides in.

• module : Name
• range : DeclarationRange

instance Lean.instInhabitedDeclarationLocation : Inhabited DeclarationLocation

instance Lean.instDecidableEqDeclarationLocation : DecidableEq DeclarationLocation

instance Lean.instReprDeclarationLocation : Repr DeclarationLocation