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

fix: mkSizeOfSpecLemmaInstance

Browse source 
It was not handling correctly constructors with implicit fields.
This commit is contained in:
Leonardo de Moura 2021-01-27 18:24:32 -08:00
parent f1a0044241
commit 70d6ea57a2
1 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Meta/SizeOf.lean
View file

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