From f4e98be1636c4ca55b07ca584967bde1f5e47f61 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 3 Mar 2022 17:36:08 -0800 Subject: [PATCH] fix: use `whnfD` at `mkNoConfusion` The `split` tactic failed at `Array.sizeOf_lt_of_mem` because the type in the equality is `Id Bool` when we write `true` instead of `id true`. --- src/Lean/Meta/AppBuilder.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index 4210a03eaa..201e601cee 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -352,7 +352,7 @@ def mkNoConfusion (target : Expr) (h : Expr) : MetaM Expr := do match type.eq? with | none => throwAppBuilderException `noConfusion ("equality expected" ++ hasTypeMsg h type) | some (α, a, b) => - let α ← whnf α + let α ← whnfD α matchConstInduct α.getAppFn (fun _ => throwAppBuilderException `noConfusion ("inductive type expected" ++ indentExpr α)) fun v us => do let u ← getLevel target return mkAppN (mkConst (Name.mkStr v.name "noConfusion") (u :: us)) (α.getAppArgs ++ #[target, a, b, h])