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

Equations

• Lean.instInhabitedDeclarationRange = { default := Lean.instInhabitedDeclarationRange.default }

def Lean.instInhabitedDeclarationRange.default : DeclarationRange

Equations

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

instance Lean.instDecidableEqDeclarationRange : DecidableEq DeclarationRange

Equations

• Lean.instDecidableEqDeclarationRange = Lean.instDecidableEqDeclarationRange.decEq

def Lean.instDecidableEqDeclarationRange.decEq (x✝ x✝¹ : DeclarationRange) : Decidable (x✝ = x✝¹)

Equations

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

def Lean.instReprDeclarationRange.repr : DeclarationRange → Nat → Format

Equations

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

instance Lean.instReprDeclarationRange : Repr DeclarationRange

Equations

• Lean.instReprDeclarationRange = { reprPrec := Lean.instReprDeclarationRange.repr }

instance Lean.instToExprDeclarationRange : ToExpr DeclarationRange

Equations

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

structure Lean.DeclarationRanges : Type

• range : DeclarationRange
• selectionRange : DeclarationRange

def Lean.instInhabitedDeclarationRanges.default : DeclarationRanges

Equations

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

instance Lean.instInhabitedDeclarationRanges : Inhabited DeclarationRanges

Equations

• Lean.instInhabitedDeclarationRanges = { default := Lean.instInhabitedDeclarationRanges.default }

instance Lean.instReprDeclarationRanges : Repr DeclarationRanges

Equations

• Lean.instReprDeclarationRanges = { reprPrec := Lean.instReprDeclarationRanges.repr }

def Lean.instReprDeclarationRanges.repr : DeclarationRanges → Nat → Format

Equations

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

instance Lean.instToExprDeclarationRanges : ToExpr DeclarationRanges

Equations

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

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

def Lean.instInhabitedDeclarationLocation.default : DeclarationLocation

Equations

• Lean.instInhabitedDeclarationLocation.default = { module := default, range := default }

instance Lean.instInhabitedDeclarationLocation : Inhabited DeclarationLocation

Equations

• Lean.instInhabitedDeclarationLocation = { default := Lean.instInhabitedDeclarationLocation.default }

instance Lean.instDecidableEqDeclarationLocation : DecidableEq DeclarationLocation

Equations

• Lean.instDecidableEqDeclarationLocation = Lean.instDecidableEqDeclarationLocation.decEq

def Lean.instDecidableEqDeclarationLocation.decEq (x✝ x✝¹ : DeclarationLocation) : Decidable (x✝ = x✝¹)

Equations

• Lean.instDecidableEqDeclarationLocation.decEq { module := a, range := a_1 } { module := b, range := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Lean.instReprDeclarationLocation.repr : DeclarationLocation → Nat → Format

Equations

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

instance Lean.instReprDeclarationLocation : Repr DeclarationLocation

Equations

• Lean.instReprDeclarationLocation = { reprPrec := Lean.instReprDeclarationLocation.repr }