max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/library/init/lean/compiler
History
Leonardo de Moura ed4cd39d59 feat(library/init/lean/compiler/ir): new IR for Lean 
It is currently implemented in C++. The plan is to move the procedures
for inserting inc/dec, reset/reuse, and inferring borrow inferences to
Lean. Another goal is to make sure new IR optimizations can be
implemented in Lean, and to avoid backend optimizations that would
have to be duplicated in each backend (e.g., `emit_proj_inc_reset_seq`
at `emit_cpp.cpp`).

cc @kha
2019-03-04 16:46:10 -08:00
..
const_folding.lean feat(library/init/lean/compiler/const_folding): const fold nat.succ and char.of_nat 2019-02-16 11:15:19 -08:00
default.lean feat(library/init/lean/compiler): add constant folding helper functions 2019-02-14 14:35:10 -08:00
ir.lean feat(library/init/lean/compiler/ir): new IR for Lean 2019-03-04 16:46:10 -08:00
util.lean feat(library/init/lean/compiler): fold nat predicates 2019-02-15 16:17:16 -08:00