Documentation

Lean.Server.GoTo

source
inductive Lean.Server.GoToKind :
Type
Instances For
    source
    instance Lean.Server.instBEqGoToKind :
    BEq GoToKind
    Equations
      source
      instance Lean.Server.instToJsonGoToKind :
      ToJson GoToKind
      Equations
        source
        instance Lean.Server.instFromJsonGoToKind :
        FromJson GoToKind
        Equations
          source
          def Lean.Server.locationLinksFromDecl (uri : Lsp.DocumentUri) (n : Name) (originRange? : Option Lsp.Range) :
          MetaM (Array Lsp.LocationLink)
          Equations
            Instances For