3 commits

Author	SHA1	Message	Date
Leonardo de Moura	14f05d2001	feat(library/init/lean/compiler): register [implementedBy] attribute using new attribute manager	2019-06-26 15:55:51 -07:00
Leonardo de Moura	0f43c2e2d9	feat(library/init/data/array/basic): efficient heterogeneous Array.map ... This commit also removes Array.hmap. Motivation: I wanted to use Array.hmap as an example in the paper, but I found it would be too distracting to explain why we had `Array.hmap` and `Array.map`. cc @kha	2019-05-25 16:32:59 -07:00
Leonardo de Moura	f6b3bc868a	fix(library/init/lean/environment, library/compiler): compilation error and add [implementedBy] attribute	2019-05-10 07:22:56 -07:00