From 632406adcd97445aff3f2b1136ca49aa9172a978 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 24 Oct 2020 16:04:13 -0700 Subject: [PATCH] fix: unused variables being included in theorems --- src/Lean/Elab/MutualDef.lean | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index f5e89faf63..71d8351149 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -161,13 +161,10 @@ private def removeUnusedVars (vars : Array Expr) (headers : Array DefViewElabHea let (_, used) ← (collectUsed headers values toLift).run {} removeUnused vars used -private def withUsedWhen {α} (vars : Array Expr) (headers : Array DefViewElabHeader) (values : Array Expr) (toLift : List LetRecToLift) - (cond : Bool) (k : Array Expr → TermElabM α) : TermElabM α := do - if cond then - let (lctx, localInsts, vars) ← removeUnusedVars vars headers values toLift - withLCtx lctx localInsts $ k vars - else - k vars +private def withUsed {α} (vars : Array Expr) (headers : Array DefViewElabHeader) (values : Array Expr) (toLift : List LetRecToLift) + (k : Array Expr → TermElabM α) : TermElabM α := do + let (lctx, localInsts, vars) ← removeUnusedVars vars headers values toLift + withLCtx lctx localInsts $ k vars private def isExample (views : Array DefView) : Bool := views.any (·.kind.isExample) @@ -583,7 +580,7 @@ def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit : let letRecsToLift ← getLetRecsToLift let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift checkLetRecsToLiftTypes funFVars letRecsToLift - withUsedWhen vars headers values letRecsToLift (not $ isTheorem views) fun vars => do + withUsed vars headers values letRecsToLift fun vars => do let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift let preDefs ← levelMVarToParamPreDecls preDefs let preDefs ← instantiateMVarsAtPreDecls preDefs