def Lean.Elab.Tactic.Do.findSpec (database : SpecAttr.SpecTheorems) (wp : Expr) : MetaM SpecAttr.SpecTheorem

def Lean.Elab.Tactic.Do.elabTermIntoSpecTheorem (stx : TSyntax `term) (expectedTy : Expr) : TacticM SpecAttr.SpecTheorem

def Lean.Elab.Tactic.Do.elabSpec (stx? : Option (TSyntax `term)) (wp : Expr) : TacticM SpecAttr.SpecTheorem

def Lean.Elab.Tactic.Do.dischargePostEntails {n : Type → Type u_1} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n] (α ps Q Q' : Expr) (goalTag : Name) : n Expr

partial def Lean.Elab.Tactic.Do.dischargeFailEntails {n : Type → Type u_1} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n] (ps Q Q' : Expr) (goalTag : Name) : n Expr

def Lean.Elab.Tactic.Do.dischargeMGoal {n : Type → Type u_1} [Monad n] [MonadLiftT MetaM n] (goal : ProofMode.MGoal) (goalTag : Name) : n Expr

def Lean.Elab.Tactic.Do.mkPreTag (goalTag : Name) : Name

def Lean.Elab.Tactic.Do.mSpec {n : Type → Type u_1} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n] (goal : ProofMode.MGoal) (elabSpecAtWP : Expr → n SpecAttr.SpecTheorem) (goalTag : Name) (mkPreTag : Name → Name := mkPreTag) : n (Expr × List MVarId)

Returns the proof and the list of new unassigned MVars.

def Lean.Elab.Tactic.Do.elabMSpecNoBind : Tactic