Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Lean.Elab.Tactic.Basic

namespace Lean.Elab.Tactic

/--
Like `evalTacticAt`, but without restoring the goal list or pruning solved goals.
Useful when these tasks are already being done in an outer loop.
-/
def 
evalTacticAtRaw: Syntax → MVarId → TacticM (List MVarId)
evalTacticAtRaw (
tac: Syntax
tac : 
Syntax: Type
Syntax) (
mvarId: MVarId
mvarId : 
MVarId: Type
MVarId) : 
TacticM: Type → Type
TacticM (
List: Type ?u.6 → Type ?u.6
List 
MVarId: Type
MVarId) := do
  
setGoals: List MVarId → TacticM Unit
setGoals [
mvarId: MVarId
mvarId]
  
evalTactic: Syntax → TacticM Unit
evalTactic 
tac: Syntax
tac
  
getGoals: TacticM (List MVarId)
getGoals