inductive Lean.Server.GoToKind : Type

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

instance Lean.Server.instBEqGoToKind : BEq GoToKind

Equations

• Lean.Server.instBEqGoToKind = { beq := Lean.Server.beqGoToKind✝ }

instance Lean.Server.instToJsonGoToKind : ToJson GoToKind

Equations

• Lean.Server.instToJsonGoToKind = { toJson := Lean.Server.toJsonGoToKind✝ }

instance Lean.Server.instFromJsonGoToKind : FromJson GoToKind

Equations

• Lean.Server.instFromJsonGoToKind = { fromJson? := Lean.Server.fromJsonGoToKind✝ }

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

Equations

• One or more equations did not get rendered due to their size.
• kind.determineTargetExprs ti = do let __do_lift ← Lean.instantiateMVars ti.expr pure #[__do_lift]

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

Equations

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

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

Equations

• Lean.Server.isInstanceProjection e = do let __do_lift ← Lean.Server.getInstanceProjectionArg? e pure __do_lift.isSome

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

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

Equations

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

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

Equations

• Lean.Server.GoToM α = ReaderT Lean.Server.GoToContext Lean.MetaM α

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

Equations

• Lean.Server.GoToM.run ctx ci lctx act = ci.runMetaM lctx (ReaderT.run act ctx)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Server.locationLinksFromOptionInfo i = Lean.Server.locationLinksFromDecl i.declName

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

Equations

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

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

Equations

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