diff --git a/server/GameServer/AbstractCtx.lean b/server/GameServer/AbstractCtx.lean index 96d215c..831c607 100644 --- a/server/GameServer/AbstractCtx.lean +++ b/server/GameServer/AbstractCtx.lean @@ -18,7 +18,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 + let (_mvars, _binderInfo, expr) ← openAbstractMVarsResult res.abstractMVarsResult lambdaLetTelescope (← instantiateMVars expr) k -- TODO: Unfornately, lambdaLetTelescope does not allow us to provide the number of arguments. -- If the goal is a function, this will not work. diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index 0569845..400c4f5 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -303,7 +303,7 @@ new.fold (fun acc a b => then acc.insert a (merge bOld b) else acc.insert a b) old -def GameLevel.merge (old : GameLevel) (new : GameLevel) : GameLevel := +def GameLevel.merge (_old : GameLevel) (new : GameLevel) : GameLevel := new -- simply override old level def World.merge (old : World) (new : World) : World :=