3 commits

Author	SHA1	Message	Date
Leonardo de Moura	1ab4c9f8bf	feat(gen/apply): simplify over-application case and avoid quadratic blowup ... The over-application doesn't occur very often in practice. The new version adds an extra "copy" step, but it avoids the quadratic blowup in code size. Xavier Leroy reports that only 5% of all calls are over-applications in his experiments. In Lean3, 6.59% of all calls performed to compile corelib are "over", and we did not implement any fancy optimization.	2018-05-12 15:10:26 -07:00
Leonardo de Moura	d02c36df18	chore(gen/apply): style	2018-05-11 18:01:58 -07:00
Leonardo de Moura	1d69493b83	feat(gen/apply): add generator for apply ... It generates the functions at `util/apply.h` that are used by the Lean runtime.	2018-05-11 17:54:09 -07:00