Environment extension for declaration ranges #
Equations
Instances For
def
Lean.addDeclarationRanges
{m : Type → Type}
[Monad m]
[MonadEnv m]
(declName : Name)
(declRanges : DeclarationRanges)
:
m Unit
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.findDeclarationRanges?
{m : Type → Type}
[Monad m]
[MonadEnv m]
[MonadLiftT BaseIO m]
(declName : Name)
:
Equations
- One or more equations did not get rendered due to their size.