satisfy unused variable linter

This commit is contained in:
Jon Eugster
2023-09-01 12:11:49 +02:00
parent 73b80e714d
commit 6371f77379
2 changed files with 2 additions and 2 deletions
+1 -1
View File
@@ -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.
+1 -1
View File
@@ -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 :=