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

fix: bug at mkSizeOfSpecLemmaInstance

Browse source 
closes #1441
This commit is contained in:
Leonardo de Moura 2022-08-07 09:24:18 -07:00
parent 0b92f625ae
commit 7dbfaf9b75
2 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -185,11 +185,13 @@ 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 _ => do
let ctorArgs := ctorApp.getAppArgs
let ctorFields := ctorArgs[ctorArgs.size - ctorInfo.numFields:]
let ctorParams := ctorArgs[:ctorInfo.numParams]
let ctorFields := ctorArgs[ctorInfo.numParams:]
let lemmaName := mkSizeOfSpecLemmaName ctorInfo.name
let lemmaInfo ← getConstInfo lemmaName
let lemmaArity ← forallTelescopeReducing lemmaInfo.type fun xs _ => return xs.size
let lemmaArgMask := mkArray (lemmaArity - ctorInfo.numFields) (none (α := Expr))
let lemmaArgMask := ctorParams.toArray.map some
let lemmaArgMask := lemmaArgMask ++ mkArray (lemmaArity - ctorInfo.numParams - ctorInfo.numFields) (none (α := Expr))
let lemmaArgMask := lemmaArgMask ++ ctorFields.toArray.map some
mkAppOptM lemmaName lemmaArgMask

2
tests/lean/run/1441.lean Normal file
View file

@ -0,0 +1,2 @@
inductive MsgEmbed where
| trace : Sum (Array MsgEmbed) Unit → MsgEmbed