From 2c22c445b197cace93605398e7ad52fc0833b793 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Wed, 24 Jul 2024 11:06:19 +0200
Subject: [PATCH] Update AbstractCtx.lean

---
 server/GameServer/AbstractCtx.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/server/GameServer/AbstractCtx.lean b/server/GameServer/AbstractCtx.lean
index ab20709..763fb9d 100644
--- a/server/GameServer/AbstractCtx.lean
+++ b/server/GameServer/AbstractCtx.lean
@@ -21,7 +21,7 @@ def abstractCtx (goal : MVarId) : MetaM AbstractCtxResult := do
 def openAbstractCtxResult (res : AbstractCtxResult) (k : Array Expr → Expr → MetaM α) : MetaM α := do
   let (_mvars, _binderInfo, expr) ← openAbstractMVarsResult res.abstractMVarsResult
   lambdaLetTelescope (← instantiateMVars expr) k
-  -- TODO: Unfornately, lambdaLetTelescope does not allow us to provide the number of arguments.
+  -- TODO: Unfortunately, lambdaLetTelescope does not allow us to provide the number of arguments.
   -- If the goal is a function, this will not work.
 
 end AbstractCtx