Documentation

Lean.DeclarationRange

  • charUtf16 : Nat

    A precomputed UTF-16 character field as in Lean.Lsp.Position. We need to store this because LSP clients want us to report the range in terms of UTF-16, but converting a Unicode codepoint stored in Lean.Position to UTF-16 requires loading and mapping the target source file, which is IO-heavy.

  • endPos : Lean.Position
  • endCharUtf16 : Nat

Store position information for declarations.

Instances For
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      Instances For
        def Lean.addDeclarationRanges {m : TypeType} [Lean.MonadEnv m] (declName : Lake.Name) (declRanges : Lean.DeclarationRanges) :
        Equations
        Instances For
          Equations
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For