Documentation

Lean.DeclarationRange

structure Lean.DeclarationRange :

Type

pos : Lean.Position
charUtf16 : Nat
endPos : Lean.Position
endCharUtf16 : Nat

instance Lean.instReprDeclarationRange :

Repr Lean.DeclarationRange

Equations

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

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.instToExprDeclarationRange :

Lean.ToExpr Lean.DeclarationRange

Equations

Lean.instToExprDeclarationRange = { toExpr := fun r => Lean.mkAppN (Lean.mkConst `Lean.DeclarationRange.mk) #[Lean.toExpr r.pos, Lean.toExpr r.charUtf16, Lean.toExpr r.endPos, Lean.toExpr r.endCharUtf16], toTypeExpr := Lean.mkConst `Lean.DeclarationRange }

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

Lean.instToExprDeclarationRanges = { toExpr := fun r => Lean.mkAppN (Lean.mkConst `Lean.DeclarationRanges.mk) #[Lean.toExpr r.range, Lean.toExpr r.selectionRange], toTypeExpr := Lean.mkConst `Lean.DeclarationRanges }

constant Lean.builtinDeclRanges :

IO.Ref (Lean.NameMap Lean.DeclarationRanges)

constant 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

Lean.findDeclarationRanges? declName = do let a ← liftM (ST.Ref.get Lean.builtinDeclRanges) let _do_jp : PUnit → m (Option Lean.DeclarationRanges) := fun y => do let env ← Lean.getEnv let a ← Lean.isRec declName if (Lean.isAuxRecursor env declName || Lean.isNoConfusion env declName || a) = true then Lean.findDeclarationRangesCore? (Lean.Name.getPrefix declName) else Lean.findDeclarationRangesCore? declName match Lean.NameMap.find? a declName with | some ranges => pure (some ranges) | x => do let y ← pure PUnit.unit _do_jp y