Documentation

Lean.Server.References

source
structure Lean.Server.Reference:
Type
source
instance Lean.Server.instInhabitedReference:
Inhabited Lean.Server.Reference
Equations
  • Lean.Server.instInhabitedReference = { default := { ident := default, aliases := default, range := default, stx := default, ci := default, info := default, isBinder := default } }
source
structure Lean.Server.RefInfo:
Type
source
def Lean.Server.RefInfo.empty:
Lean.Server.RefInfo
Equations
source
def Lean.Server.RefInfo.addRef:
Lean.Server.RefInfo → Lean.Server.Reference → Lean.Server.RefInfo
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Server.RefInfo.instCoeRefInfoRefInfo:
Coe Lean.Server.RefInfo Lean.Lsp.RefInfo
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.ModuleRefs:
Type
Equations
source
def Lean.Server.ModuleRefs.addRef (self : Lean.Server.ModuleRefs) (ref : Lean.Server.Reference) :
Lean.Server.ModuleRefs
Equations
source
instance Lean.Server.ModuleRefs.instCoeModuleRefsModuleRefs:
Coe Lean.Server.ModuleRefs Lean.Lsp.ModuleRefs
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Lsp.RefInfo.empty:
Lean.Lsp.RefInfo
Equations
source
def Lean.Lsp.RefInfo.merge (a : Lean.Lsp.RefInfo) (b : Lean.Lsp.RefInfo) :
Lean.Lsp.RefInfo
Equations
source
def Lean.Lsp.RefInfo.contains (self : Lean.Lsp.RefInfo) (pos : Lean.Lsp.Position) :
Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Lsp.RefInfo.contains.contains (range : Lean.Lsp.Range) (pos : Lean.Lsp.Position) :
Bool
Equations
source
def Lean.Lsp.ModuleRefs.findAt (self : Lean.Lsp.ModuleRefs) (pos : Lean.Lsp.Position) :
Array Lean.Lsp.RefIdent
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.Server.Ilean:
Type

Content of individual .ilean files

source
instance Lean.Server.instFromJsonIlean:
Lean.FromJson Lean.Server.Ilean
Equations
source
instance Lean.Server.instToJsonIlean:
Lean.ToJson Lean.Server.Ilean
Equations
source
def Lean.Server.Ilean.load (path : System.FilePath) :
IO Lean.Server.Ilean
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.identOf:
Lean.Elab.Info → Option (Lean.Lsp.RefIdent × Bool)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.findReferences (text : Lean.FileMap) (trees : Array Lean.Elab.InfoTree) :
Array Lean.Server.Reference
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.combineFvars (refs : Array Lean.Server.Reference) :
Array Lean.Server.Reference

The FVarIds of a function parameter in the function's signature and body differ. However, they have TermInfo nodes with binder := true in the exact same position. Moreover, macros such as do-reassignment x := e may create chains of variable definitions where a helper definition overlaps with a use of a variable.

This function changes every such group to use a single FVarId (the head of the chain/DAG) and gets rid of duplicate definitions.

Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Server.combineFvars.findCanonicalBinder (idMap : Std.HashMap Lean.FVarId Lean.FVarId) (id : Lean.FVarId) :
Lean.FVarId
source
def Lean.Server.combineFvars.applyIdMap:
Std.HashMap Lean.FVarId Lean.FVarId → Lean.Lsp.RefIdent → Lean.Lsp.RefIdent
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.dedupReferences (refs : Array Lean.Server.Reference) :
Array Lean.Server.Reference
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.findModuleRefs (text : Lean.FileMap) (trees : Array Lean.Elab.InfoTree) (localVars : optParam Bool true) :
Lean.Server.ModuleRefs
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.Server.References:
Type
source
def Lean.Server.References.empty:
Lean.Server.References
Equations
source
def Lean.Server.References.addIlean (self : Lean.Server.References) (path : System.FilePath) (ilean : Lean.Server.Ilean) :
Lean.Server.References
Equations
source
def Lean.Server.References.removeIlean (self : Lean.Server.References) (path : System.FilePath) :
Lean.Server.References
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.References.updateWorkerRefs (self : Lean.Server.References) (name : Lean.Name) (version : Nat) (refs : Lean.Lsp.ModuleRefs) :
Lean.Server.References
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.References.finalizeWorkerRefs (self : Lean.Server.References) (name : Lean.Name) (version : Nat) (refs : Lean.Lsp.ModuleRefs) :
Lean.Server.References
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.References.removeWorkerRefs (self : Lean.Server.References) (name : Lean.Name) :
Lean.Server.References
Equations
source
def Lean.Server.References.allRefs (self : Lean.Server.References) :
Std.HashMap Lean.Name Lean.Lsp.ModuleRefs
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.References.findAt (self : Lean.Server.References) (module : Lean.Name) (pos : Lean.Lsp.Position) :
Array Lean.Lsp.RefIdent
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.References.referringTo (self : Lean.Server.References) (identModule : Lean.Name) (ident : Lean.Lsp.RefIdent) (srcSearchPath : Lean.SearchPath) (includeDefinition : optParam Bool true) :
IO (Array Lean.Lsp.Location)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.References.definitionOf? (self : Lean.Server.References) (ident : Lean.Lsp.RefIdent) (srcSearchPath : Lean.SearchPath) :
IO (Option Lean.Lsp.Location)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Server.References.definitionsMatching {α : Type} (self : Lean.Server.References) (srcSearchPath : Lean.SearchPath) (filter : Lean.Name → Option α) (maxAmount? : optParam (Option Nat) none) :
IO (Array (α × Lean.Lsp.Location))
Equations
  • One or more equations did not get rendered due to their size.