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.