From 222cb035d1d0a9f8bda842b8a1f3bab967a8366f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 11 Apr 2024 15:04:36 -0700
Subject: [PATCH] feat: Add library bindings for calc

---
 Pantograph/Library.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 0febba4..ff365b2 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -178,6 +178,10 @@ def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult :=
 def goalConvExit (state: GoalState): Lean.CoreM TacticResult :=
   runTermElabM <| state.convExit
 
+@[export pantograph_goal_calc_m]
+def goalCalc (state: GoalState) (goalId: Nat) (pred: String): Lean.CoreM TacticResult :=
+  runTermElabM <| state.tryCalc goalId pred
+
 @[export pantograph_goal_focus]
 def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
   state.focus goalId