def Iris.Std.apply' (goal : Lean.MVarId) (name : Lean.Name) : Lean.Elab.Tactic.TacticM (Option (List Lean.MVarId))

Apply the theorem with the name name to the goal goal. The flag recover is set to false and the transparency mode is set to reducible. Only non-dependent arguments of the applied theorem are turned into goals.

Equations

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

def Iris.Std.findGoalFromTag? (tag : Lean.Name) : Lean.Elab.Tactic.TacticM (Option Lean.MVarId)

Find the goal with the tag tag.

Equations

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

def Iris.Std.withFocus {α : Type} (goal : Lean.MVarId) (f : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

Execute the function f with the single goal goal and restore all current goals after the execution.

Equations

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