def
Lean.Elab.getDeclarationRange
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadFileMap m]
(stx : Lean.Syntax)
:

## Equations

- One or more equations did not get rendered due to their size.

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.

def
Lean.Elab.addDeclarationRanges
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadFileMap m]
(declName : Lean.Name)
(stx : Lean.Syntax)
:

m Unit

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.

def
Lean.Elab.addAuxDeclarationRanges
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadFileMap m]
(declName : Lean.Name)
(stx : Lean.Syntax)
(header : Lean.Syntax)
:

m Unit

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.