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.Meta.Grind.markGrindName (userName : Name) : Name

Equations

• Lean.Meta.Grind.markGrindName userName = userName.str Lean.Meta.Grind.grindMark✝

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.