def Iris.ProofMode.Hyps.rename {u : Lean.Level} (oldUniq new : Lean.Name) {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e : Q(«$prop»)} : Hyps bi e → Option (Hyps bi e)

Equations

• One or more equations did not get rendered due to their size.
• Iris.ProofMode.Hyps.rename oldUniq new (Iris.ProofMode.Hyps.emp x_3) = none
• Iris.ProofMode.Hyps.rename oldUniq new (Iris.ProofMode.Hyps.hyp tm name uniq p ty x_3) = if (oldUniq == uniq) = true then some (Iris.ProofMode.Hyps.mkHyp bi new uniq p ty x✝) else none

def Iris.ProofMode.«tacticIrename__=>__» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Iris.ProofMode.«tacticIrename:__=>__» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.