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

## 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

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

m Unit

Store the `range`

and `selectionRange`

for `declName`

where `stx`

is the whole syntax object describing `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

def
Lean.Elab.addAuxDeclarationRanges
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadFileMap m]
(declName : Lake.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.