From 95bd55bc218b8a0e96466e810c371c3cee0b132d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Apr 2022 11:21:50 -0700 Subject: [PATCH] chore: fix typo and remove unnecessary discriminant --- src/Lean/Widget/InteractiveGoal.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean index 961bad568e..4709ab31e3 100644 --- a/src/Lean/Widget/InteractiveGoal.lean +++ b/src/Lean/Widget/InteractiveGoal.lean @@ -87,15 +87,15 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do 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. - -- Then should be remove after we rewrite the compiler in Lean + -- They should be removed after we rewrite the compiler in Lean let rec pushPending (ids : Array Name) (type? : Option Expr) (hyps : Array InteractiveHypothesis) : MetaM (Array InteractiveHypothesis) := if ids.isEmpty then pure hyps else - match ids, type? with - | _, none => pure hyps - | _, some type => addInteractiveHypothesis hyps ids type + match type? with + | none => pure hyps + | some type => addInteractiveHypothesis hyps ids type let rec ppVars (varNames : Array Name) (prevType? : Option Expr) (hyps : Array InteractiveHypothesis) (localDecl : LocalDecl) : MetaM (Array Name × Option Expr × Array InteractiveHypothesis) := do if hiddenProp.contains localDecl.fvarId then