max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/library/equations_compiler
History
Leonardo de Moura 69070f43eb chore(library/local_context): remove user_name indexing 
The datastructures at `local_context` used to manage used user_names
introduce a lot of overhead. They do guarantee that `get_unused_name` is
`O(log(n))`, but they slowdown much more common operations such as:
local declaration creation/deletion. We create/delete local declarations
much more often than we use `get_unused_name`.

The corelib build time is now 34.18 secs on my desktop. It was 39.5 secs.
2018-10-17 09:24:40 -07:00
..
CMakeLists.txt feat(library/equations_compiler): add pack_mutual 2017-05-18 15:29:51 -07:00
compiler.cpp feat(library/compiler): new compiler entry point (skeleton) 2018-10-05 17:30:27 -07:00
compiler.h feat(library/compiler): new compiler entry point (skeleton) 2018-10-05 17:30:27 -07:00
elim_match.cpp chore(library,frontends/lean): use is_constructor, is_recursor, is_inductive helper functions 2018-09-07 20:36:42 -07:00
elim_match.h feat(library/equations_compiler): add new cache support to equation compiler 2018-02-21 15:04:20 -08:00
equations.cpp feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
equations.h chore(library/equations_compiler): remove equations macro 2018-06-19 13:41:08 -07:00
init_module.cpp feat(library/compiler): new compiler entry point (skeleton) 2018-10-05 17:30:27 -07:00
init_module.h
pack_domain.cpp refactor(kernel/expr): remove mlocal_* functions 2018-06-22 14:25:31 -07:00
pack_domain.h chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
pack_mutual.cpp refactor(kernel/expr): remove mlocal_* functions 2018-06-22 14:25:31 -07:00
pack_mutual.h chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
structural_rec.cpp chore(kernel): remove expr.quote constructor 2018-09-07 22:08:08 -07:00
structural_rec.h feat(library/equations_compiler): add new cache support to equation compiler 2018-02-21 15:04:20 -08:00
unbounded_rec.cpp feat(library/compiler/compiler): switch to new compiler frontend 2018-10-08 17:38:17 -07:00
unbounded_rec.h feat(library/equations_compiler): add new cache support to equation compiler 2018-02-21 15:04:20 -08:00
util.cpp chore(library/local_context): remove user_name indexing 2018-10-17 09:24:40 -07:00
util.h chore(library/equations_compiler): do not generate equation lemmas 2018-08-23 14:04:37 -07:00
wf_rec.cpp fix(library/equations_compiler/wf_rec): do not generate code for auxiliary *._pack functions added by equation compiler 2018-09-12 22:05:52 -07:00
wf_rec.h feat(library/equations_compiler): add new cache support to equation compiler 2018-02-21 15:04:20 -08:00