From 1868cea536ecea8ccde26cc2b76c522b5ee00ec8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Sep 2021 07:22:14 -0700 Subject: [PATCH] fix: "stuck at universe contraint" issues --- src/Lean/Meta/IndPredBelow.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean index 04d6b985be..2a36cd3fdc 100644 --- a/src/Lean/Meta/IndPredBelow.lean +++ b/src/Lean/Meta/IndPredBelow.lean @@ -107,14 +107,14 @@ partial def mkCtorType where addHeaderVars (vars : Variables) := do let headersWithNames ← ctx.headers.mapIdxM fun idx header => - (ctx.belowNames[idx], fun _ => pure header) + (ctx.belowNames[idx], fun _ : Array Expr => pure header) withLocalDeclsD headersWithNames fun xs => addMotives { vars with indVal := xs } addMotives (vars : Variables) := do let motiveBuilders ← ctx.motives.mapM fun (motiveName, motiveType) => - (motiveName, BinderInfo.implicit, fun _ => + (motiveName, BinderInfo.implicit, fun _ : Array Expr => instantiateForall motiveType vars.params) withLocalDecls motiveBuilders fun xs => modifyBinders { vars with target := vars.target ++ xs, motives := xs } 0 @@ -341,7 +341,7 @@ where then mkFreshUserName s!"ih_{idx.val.succ}" else mkFreshUserName "ih" let ih ← instantiateForall motive.2 params - let mkDomain _ := + let mkDomain (_ : Array Expr) : MetaM Expr := forallTelescope ih fun ys t => do let levels := ctx.typeInfos[idx].levelParams.map mkLevelParam let args := params ++ motives ++ ys