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.

def Lean.Meta.Grind.markGrindName (userName : Name) : Name

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.

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.