Low-level delta expansion. It is used to implement equation lemmas and elimination principles for recursive definitions.

## Equations

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

## Instances For

Delta expand declarations that satisfy `p`

at `mvarId`

type.

## Equations

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

## Instances For

def
Lean.MVarId.deltaLocalDecl
(mvarId : Lean.MVarId)
(fvarId : Lean.FVarId)
(p : Lake.Name → Bool)
:

Delta expand declarations that satisfy `p`

at `fvarId`

type.

## Equations

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