From cea53fc53e9352b7c832735856cdc7299aae44e4 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 1 Jun 2022 10:44:37 -0400 Subject: [PATCH] fix: tests Caused by a classic imperative programming bug oops --- src/Lean/Widget/InteractiveGoal.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean index 2f0e19d8f8..479ec77e84 100644 --- a/src/Lean/Widget/InteractiveGoal.lean +++ b/src/Lean/Widget/InteractiveGoal.lean @@ -107,8 +107,6 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do let lctx : LocalContext := lctx.sanitizeNames.run' { options := (← getOptions) } withLCtx lctx mvarDecl.localInstances do let (hidden, hiddenProp) ← ToHide.collect mvarDecl.type - -- The following two `let rec`s are being used to control the generated code size. - -- They should be removed after we rewrite the compiler in Lean let pushPending (ids : Array (Name × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesis) : MetaM (Array InteractiveHypothesis) := if ids.isEmpty then @@ -122,7 +120,7 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do let mut hyps : Array InteractiveHypothesis := #[] for localDecl in lctx do if !ppAuxDecls && localDecl.isAuxDecl || hidden.contains localDecl.fvarId then - pure () + continue else if hiddenProp.contains localDecl.fvarId then -- localDecl has an inaccessible name and @@ -137,12 +135,12 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do | LocalDecl.cdecl index fvarId varName type _ => let varName := varName.simpMacroScopes let type ← instantiateMVars type - prevType? := some type if prevType? == none || prevType? == some type then varNames := varNames.push (varName, fvarId) else hyps ← pushPending varNames prevType? hyps varNames := #[(varName, fvarId)] + prevType? := some type | LocalDecl.ldecl index fvarId varName type val _ => do let varName := varName.simpMacroScopes hyps ← pushPending varNames prevType? hyps