From 85eb42207c4d234714e87e00de3e2cc35a103483 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 14 Dec 2023 05:52:12 -0800
Subject: [PATCH] fix: env_add monads

---
 Pantograph.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index bdaa57c..ad3b221 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -105,14 +105,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let env ← Lean.MonadEnv.getEnv
     let type ← match syntax_from_str env args.type with
       | .ok syn => do
-        match ← syntax_to_expr syn with
+        match ← (syntax_to_expr syn |> runTermElabM) with
         | .error e => return .error $ errorExpr e
         | .ok expr => pure expr
       | .error e => return .error $ errorExpr e
     let value ← match syntax_from_str env args.value with
       | .ok syn => do
         try
-          let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
+          let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) |> runTermElabM
           pure $ expr
         catch ex => return .error $ errorExpr (← ex.toMessageData.toString)
       | .error e => return .error $ errorExpr e