Documentation

Lean.Elab.DeclarationRange

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    For most builtin declarations, the selection range is just its name, which is stored in the second position. Example:

    "def " >> declId >> optDeclSig >> declVal
    

    If the declaration name is absent, we use the keyword instead. This function converts the given Syntax into one that represents its "selection range".

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Store the range and selectionRange for declName where stx is the whole syntax object decribing declName. This method is for the builtin declarations only. User-defined commands should use Lean.addDeclarationRanges to store this information for their commands.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Auxiliary method for recording ranges for auxiliary declarations (e.g., fields, nested declarations, etc.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For