Documentation
Lean
.
Server
.
Completion
.
CompletionUtils
Search
Google site search
return to top
source
Imports
Init.Prelude
Lean.Elab.InfoTree.Types
Imported by
Lean
.
Server
.
Completion
.
HoverInfo
Lean
.
Server
.
Completion
.
ContextualizedCompletionInfo
source
inductive
Lean
.
Server
.
Completion
.
HoverInfo
:
Type
after :
Lean.Server.Completion.HoverInfo
inside
(delta :
Nat
)
:
Lean.Server.Completion.HoverInfo
Instances For
source
structure
Lean
.
Server
.
Completion
.
ContextualizedCompletionInfo
:
Type
hoverInfo :
Lean.Server.Completion.HoverInfo
ctx :
Lean.Elab.ContextInfo
info :
Lean.Elab.CompletionInfo
Instances For