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

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.

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.