source
def Lean.Meta.Grind.getOriginalName? (name : Name) :
Option Name

Return `some originalName` if `name` is a name generated by `markAccessible`. `originalName` is the original name before `markAccessible` was invoked.

Equations

- Lean.Meta.Grind.getOriginalName? (p.str s) = if (s == Lean.Meta.Grind.grindMark✝) = true then some p else none
- Lean.Meta.Grind.getOriginalName? name = none

Instances For

source
def Lean.MVarId.markAccessible (mvarId : MVarId) :
MetaM MVarId

Helper tactic for marking accessible names in the local context. This is a trick used during `grind` preprocessing when `clean := false`. Recall that during preprocessing, `grind` reverts all hypotheses and reintroduce them while normalizing and performing eager case splitting. When `clean := false`, we create a fresh user name unless the name was "marked" by this function.

Equations

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

Instances For

source
def Lean.MVarId.revertAll (mvarId : MVarId) :
MetaM MVarId

Reverts all free variables in the goal `mvarId`. Remark: Auxiliary local declarations are cleared. The `grind` tactic also clears them, but this tactic can be used independently by users.

Equations

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

Instances For