Documentation

Lean.Server.Completion

Equations
• itemsMain :
• itemsOther :
Instances For
@[inline]
Equations
def Lean.Server.Completion.matchNamespace (ns : Lean.Name) (nsFragment : Lean.Name) (danglingDot : Bool) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Server.Completion.find?.choose (hoverPos : String.Pos) (fileMap : Lean.FileMap) (hoverLine : Nat) (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.Info) :
Equations
• One or more equations did not get rendered due to their size.