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 029766495b feat(library/equations_compiler/util): try to improve performance of lemma generation 
There are still performance problems. Lemma generation is fine, but the
kernel is timing out when checking the lemma. We need to provide hints
to the kernel to avoid the performance problem.
2016-09-03 13:24:44 -07:00
..
CMakeLists.txt feat(library/equations_compiler): add elim_match skeleton 2016-08-17 21:38:23 -07:00
compiler.cpp feat(library/equations_compiler/structural_rec): generate brec_on-based function 2016-08-29 15:58:13 -07:00
compiler.h feat(library/equations_compiler/elim_match): refactor 'program' structure 2016-08-18 14:17:49 -07:00
elim_match.cpp feat(library/equations_compiler/elim_match): use if-then-else when next pattern for every equation is a variable or value 2016-09-03 13:22:25 -07:00
elim_match.h feat(library/equations_compiler/structural_rec): generate eqn lemmas at structural_rec 2016-08-31 09:07:17 -07:00
equations.cpp feat(frontends/lean): use equations_header 2016-08-30 13:45:59 -07:00
equations.h feat(frontends/lean): use equations_header 2016-08-30 13:45:59 -07:00
init_module.cpp feat(library/equations_compiler): use defeq simplifier to cleanup types of automatically synthesized lemmas 2016-08-31 15:54:03 -07:00
init_module.h refactor(library/equations_compiler): isolate old equations compiler 2016-08-11 10:08:30 -07:00
old_compiler.cpp refactor(library/equations_compiler): isolate old equations compiler 2016-08-11 10:08:30 -07:00
old_compiler.h refactor(library/equations_compiler): isolate old equations compiler 2016-08-11 10:08:30 -07:00
old_goal.cpp refactor(library): move equations to equations_compiler 2016-08-11 10:08:30 -07:00
old_goal.h refactor(library): move equations to equations_compiler 2016-08-11 10:08:30 -07:00
old_inversion.cpp refactor(library): move equations to equations_compiler 2016-08-11 10:08:30 -07:00
old_inversion.h refactor(library): move equations to equations_compiler 2016-08-11 10:08:30 -07:00
pack_domain.cpp feat(library/equations_compiler/pack_domain): avoid unnecessary 'unit' type when packing 2016-08-16 13:59:47 -07:00
pack_domain.h refactor(library/equations_compiler): move pack_domain to new module 2016-08-15 08:22:23 -07:00
structural_rec.cpp feat(library/equations_compiler): prove equation lemmas that use if-then-else 2016-09-03 13:23:09 -07:00
structural_rec.h feat(library/equations_compiler/structural_rec): generate brec_on-based function 2016-08-29 15:58:13 -07:00
unbounded_rec.cpp feat(library/equations_compiler): add unbounded_rec 2016-08-16 12:54:54 -07:00
unbounded_rec.h feat(library/equations_compiler): add unbounded_rec 2016-08-16 12:54:54 -07:00
util.cpp feat(library/equations_compiler/util): try to improve performance of lemma generation 2016-09-03 13:24:44 -07:00
util.h feat(library/equations_compiler): prove equation lemmas that use if-then-else 2016-09-03 13:23:09 -07:00