max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: "stuck at universe contraint" issues

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-20 07:22:14 -07:00
parent 11cdc65820
commit 1868cea536
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Meta/IndPredBelow.lean
View file

@ -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