From 34a4bf5b7321f413e12c1c1cd814d0b0e1a52e29 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 22:12:04 -0800 Subject: [PATCH] feat: Export GoalState.tryTactic --- Pantograph/Goal.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 8d29aa8..ac09109 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -215,6 +215,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E return .failure #[← exception.toMessageData.toString] /-- Execute a string tactic on given state. Restores TermElabM -/ +@[export pantograph_goal_state_try_tactic_m] protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String): Elab.TermElabM TacticResult := do state.restoreElabM