max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Compiler/LCNF/Simp
History
Leonardo de Moura 5c925f9345 feat: add functions to create small arrays and use them in the constant folder 
It reduces the code generated for functions using a bunch
of quotations. For example, the size of
`Lean.Elab.Term.Do.ToTerm.matchNestedTermResult` went from 2348 to 1507
2022-09-28 22:00:50 -07:00
..
Basic.lean
Config.lean feat: track recursively inlining 2022-09-27 16:26:49 -07:00
ConstantFold.lean feat: add functions to create small arrays and use them in the constant folder 2022-09-28 22:00:50 -07:00
DefaultAlt.lean
FunDeclInfo.lean
InlineCandidate.lean feat: track recursively inlining 2022-09-27 16:26:49 -07:00
InlineProj.lean fix: missing eraseCode at inlineProjInst? 2022-09-27 16:26:49 -07:00
JpCases.lean feat: track recursively inlining 2022-09-27 16:26:49 -07:00
Main.lean feat: track recursively inlining 2022-09-27 16:26:49 -07:00
SimpM.lean feat: constructor => discriminant optimization 2022-09-28 21:14:19 -07:00
SimpValue.lean feat: constructor => discriminant optimization 2022-09-28 21:14:19 -07:00
Used.lean