From 70d6ea57a2fc3eb918fb5465ae100a050a0579dd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Jan 2021 18:24:32 -0800 Subject: [PATCH] fix: `mkSizeOfSpecLemmaInstance` It was not handling correctly constructors with implicit fields. --- src/Lean/Meta/SizeOf.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean index 3eeb21b77c..3baab742c2 100644 --- a/src/Lean/Meta/SizeOf.lean +++ b/src/Lean/Meta/SizeOf.lean @@ -163,10 +163,14 @@ def mkSizeOfSpecLemmaName (ctorName : Name) : Name := def mkSizeOfSpecLemmaInstance (ctorApp : Expr) : MetaM Expr := matchConstCtor ctorApp.getAppFn (fun _ => throwError! "failed to apply 'sizeOf' spec, constructor expected{indentExpr ctorApp}") fun ctorInfo ctorLevels => do + let ctorArgs := ctorApp.getAppArgs + let ctorFields := ctorArgs[ctorArgs.size - ctorInfo.numFields:] let lemmaName := mkSizeOfSpecLemmaName ctorInfo.name - let ctorArgs := ctorApp.getAppArgs - let ctorFields := ctorArgs[ctorArgs.size - ctorInfo.numFields:] - mkAppM lemmaName ctorFields + let lemmaInfo ← getConstInfo lemmaName + let lemmaArity ← forallTelescopeReducing lemmaInfo.type fun xs _ => return xs.size + let lemmaArgMask := mkArray (lemmaArity - ctorInfo.numFields) (none (α := Expr)) + let lemmaArgMask := lemmaArgMask ++ ctorFields.toArray.map some + mkAppOptM lemmaName lemmaArgMask /- SizeOf spec theorem for nested inductive types -/ namespace SizeOfSpecNested