Documentation

Lean.Elab.Tactic.RenameInaccessibles

source
def Lean.Elab.Tactic.renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray `Lean.binderIdent) :
TermElabM MVarId
Equations
    Instances For