Additions to Lean.Elab.Tactic.Basic

def Lean.Elab.Tactic.getMainTarget'' : TacticM Expr

Return expected type for the main goal, cleaning up annotations, using Lean.MVarId.getType''. Remark: note that MVarId.getType' uses whnf instead of cleanupAnnotations, and MVarId.getType'' also uses cleanupAnnotations

Equations

• Lean.Elab.Tactic.getMainTarget'' = do let __do_lift ← Lean.Elab.Tactic.getMainGoal liftM __do_lift.getType''

def Lean.Elab.Tactic.commitIfNoExPreservingInfoAndMessages {α : Type} (x : TacticM α) : TacticM α

Runs x, and if x throws an exception, rewinds the tactic state except for the InfoState and Messages. This means that hovers and error messages created within x are preserved.

Note: x is run under withSaveInfoContext in order to propagate hovers and messages correctly. This means that pre-existing infotrees are not accessible from within x.

Equations

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