diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index f73200252410..ec7bccbe941a 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -778,7 +778,8 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : let indFVar := indFVars[i]! Term.addLocalVarInfo views[i]!.declId indFVar let r := rs[i]! - let type := r.type |>.abstract r.params |>.instantiateRev params + let type ← instantiateMVars r.type + let type := type |>.abstract r.params |>.instantiateRev params let type ← mkForallFVars params type let ctors ← withExplicitToImplicit params (elabCtors indFVars indFVar params r) indTypesArray := indTypesArray.push { name := r.view.declName, type, ctors } diff --git a/tests/lean/run/3242.lean b/tests/lean/run/3242.lean index c9ce4f9e1dee..2944ff72236a 100644 --- a/tests/lean/run/3242.lean +++ b/tests/lean/run/3242.lean @@ -11,3 +11,12 @@ inductive R (F: α → α → Prop) (a : α) : α → Prop where inductive And₂ (F: α → α → Prop) (a : α) : α → (Nat → α) → Nat → Prop where | mk (b : α) (f : Nat → α) (n : Nat): R F a (f n) → F (f n) b → And₂ F a b f n end + + +structure Salg (n k: Nat) where + D: Type + +mutual +inductive Ins (salg: Salg n k) : salg.D → Prop +inductive Out (salg: Salg n k) : salg.D → Prop +end