lean4-htt/src/library/equations_compiler
2017-02-17 13:45:57 +01:00
..
CMakeLists.txt chore(library/equations_compiler): remove old equation compiler 2016-09-19 17:13:30 -07:00
compiler.cpp fix(library): change API and make sure we don't crash when searching for a non existing local decl 2017-02-07 09:38:19 -08:00
compiler.h feat(library/equations_compiler/elim_match): refactor 'program' structure 2016-08-18 14:17:49 -07:00
elim_match.cpp fix(library/equations_compiler): structural recursion and partial equations 2017-02-16 14:51:31 -08:00
elim_match.h feat(library/equations_compiler): add mk_nonrec 2016-09-08 14:09:05 -07:00
equations.cpp feat(library/equations_compiler): add flag for marking equations that we should not report an error if they are not used 2017-02-05 19:26:45 -08:00
equations.h feat(library/equations_compiler): add flag for marking equations that we should not report an error if they are not used 2017-02-05 19:26:45 -08: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
pack_domain.cpp refactor(library): rename pr1/pr2 ==> fst/snd 2016-09-21 09:48:39 -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 fix(library/equations_compiler): structural recursion and partial equations 2017-02-16 14:51:31 -08: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 support for meta_definitions 2016-09-18 10:52:38 -07:00
unbounded_rec.h feat(library/equations_compiler): add support for meta_definitions 2016-09-18 10:52:38 -07:00
util.cpp refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
util.h fix(library/equations_compiler): structural recursion and partial equations 2017-02-16 14:51:31 -08:00