Additions to Lean.Elab.Tactic.Basic

def Lean.Elab.Tactic.getMainTarget'' : Lean.Elab.Tactic.TacticM Lean.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 (Lean.MVarId.getType'' __do_lift)

def Lean.Elab.Tactic.doneWithScope (scope : Lean.MessageData) : Lean.Elab.Tactic.TacticM Unit

Like done but takes a scope (e.g. a tactic name) as an argument to produce more detailed error messages.

Equations

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

def Lean.Elab.Tactic.focusAndDoneWithScope {α : Type} (scope : Lean.MessageData) (tactic : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

Like focusAndDone but takes a scope (e.g. tactic name) as an argument to produce more detailed error messages.

Equations

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