max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/library/compiler
History
Leonardo de Moura 4b6583ae9f refactor(util): move mpz/mpq to util 
The new lean_obj objects will be defined at util.
Reason: we will define `name`, `options`, `format`, ... on top of lean_obj.
lean_obj depends on mpz.
Remark: lean_obj will replace vm_obj.
2018-04-12 16:43:11 -07:00
..
CMakeLists.txt chore(library/compiler): remove obsolete optimization step 2018-02-02 08:39:39 -08:00
comp_irrelevant.cpp feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
comp_irrelevant.h chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
compiler_step_visitor.cpp chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
compiler_step_visitor.h chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
cse.cpp chore(*): rename expr_struct_* to expr_* 2018-04-09 12:55:48 -07:00
cse.h feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
elim_recursors.cpp chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
elim_recursors.h feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
elim_unused_lets.cpp chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
elim_unused_lets.h feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
erase_irrelevant.cpp chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
erase_irrelevant.h feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
eta_expansion.cpp chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
eta_expansion.h feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
extract_values.cpp chore(*): rename expr_struct_* to expr_* 2018-04-09 12:55:48 -07:00
extract_values.h feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
init_module.cpp feat(*): C++ code generator 2016-12-05 16:11:41 -08:00
init_module.h
inliner.cpp chore(library/compiler/inliner): fix weird include 2018-03-29 13:08:43 -07:00
inliner.h feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
lambda_lifting.cpp chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
lambda_lifting.h feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
nat_value.cpp refactor(util): move mpz/mpq to util 2018-04-12 16:43:11 -07:00
nat_value.h refactor(util): move mpz/mpq to util 2018-04-12 16:43:11 -07:00
preprocess.cpp chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
preprocess.h feat(library/equations_compiler): meta mutual definitions 2017-10-30 15:06:12 -07:00
procedure.h
rec_fn_macro.cpp fix(library/compiler/rec_fn_macro): do not type-check in non-meta declarations 2017-12-17 15:47:52 +01:00
rec_fn_macro.h
reduce_arity.cpp feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
reduce_arity.h feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
simp_inductive.cpp chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
simp_inductive.h feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
util.cpp chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
util.h chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
vm_compiler.cpp feat(util/name_generator): name generator prefix bookkeeping 2018-02-21 15:04:19 -08:00
vm_compiler.h feat(library/equations_compiler): meta mutual definitions 2017-10-30 15:06:12 -07:00