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