inductive Lean.Server.GoToKind : Type

• declaration : GoToKind
• definition : GoToKind
• type : GoToKind

def Lean.Server.instBEqGoToKind.beq : GoToKind → GoToKind → Bool

@[instance_reducible]

instance Lean.Server.instBEqGoToKind : BEq GoToKind

@[instance_reducible]

instance Lean.Server.instToJsonGoToKind : ToJson GoToKind

def Lean.Server.instToJsonGoToKind.toJson : GoToKind → Json

@[instance_reducible]

instance Lean.Server.instFromJsonGoToKind : FromJson GoToKind

def Lean.Server.instFromJsonGoToKind.fromJson : Json → Except String GoToKind

def Lean.Server.GoToKind.determineTargetExprs (kind : GoToKind) (ti : Elab.TermInfo) : MetaM (Array Expr)

def Lean.Server.getInstanceProjectionArg? (e : Expr) : MetaM (Option Expr)

def Lean.Server.isInstanceProjection (e : Expr) : MetaM Bool

def Lean.Server.isInstanceProjectionInfoFor (kind : GoToKind) (ti1 ti2 : Elab.TermInfo) : MetaM Bool

Checks whether ti1 is an instance projection info that subsumes ti2.

structure Lean.Server.GoToContext : Type

• doc : DocumentMeta
• kind : GoToKind
• infoTree? : Option Elab.InfoTree
• originInfo? : Option Elab.Info
• children : PersistentArray Elab.InfoTree

@[reducible, inline]

abbrev Lean.Server.GoToM (α : Type) : Type

def Lean.Server.GoToM.run {α : Type} (ctx : GoToContext) (ci : Elab.ContextInfo) (lctx : LocalContext) (act : GoToM α) : IO α

def Lean.Server.locationLinksFromDecl (declName : Name) : GoToM (Array Lsp.LeanLocationLink)

def Lean.Server.locationLinksFromBinder (id : FVarId) : GoToM (Array Lsp.LeanLocationLink)

def Lean.Server.locationLinksFromImport (i : Elab.CommandInfo) : GoToM (Array Lsp.LeanLocationLink)

def Lean.Server.locationLinksDefault : GoToM (Array Lsp.LeanLocationLink)

def Lean.Server.locationLinksFromErrorNameInfo (eni : Elab.ErrorNameInfo) : GoToM (Array Lsp.LeanLocationLink)

def Lean.Server.locationLinksFromInstanceProjection (e : Expr) : GoToM (Array Lsp.LeanLocationLink)

def Lean.Server.locationLinksFromTermInfo (ti : Elab.TermInfo) : GoToM (Array Lsp.LeanLocationLink)

def Lean.Server.locationLinksFromDelabTermInfo (dti : Elab.DelabTermInfo) : GoToM (Array Lsp.LeanLocationLink)

def Lean.Server.locationLinksFromFieldInfo (fi : Elab.FieldInfo) : GoToM (Array Lsp.LeanLocationLink)

def Lean.Server.locationLinksFromOptionInfo (i : Elab.OptionInfo) : GoToM (Array Lsp.LeanLocationLink)

def Lean.Server.locationLinksFromCommandInfo (i : Elab.CommandInfo) : GoToM (Array Lsp.LeanLocationLink)

def Lean.Server.locationLinksOfInfo (doc : DocumentMeta) (kind : GoToKind) (ictx : Elab.InfoWithCtx) (infoTree? : Option Elab.InfoTree := none) : IO (Array Lsp.LeanLocationLink)