| .. |
|
CMakeLists.txt
|
chore(library/equations_compiler): remove old equation compiler
|
2016-09-19 17:13:30 -07:00 |
|
compiler.cpp
|
fix(library/equations_compiler/compiler): fix #1315
|
2017-01-16 20:01:25 -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/elim_match): fix #1318
|
2017-01-18 08:21:53 -08:00 |
|
elim_match.h
|
feat(library/equations_compiler): add mk_nonrec
|
2016-09-08 14:09:05 -07:00 |
|
equations.cpp
|
refactor(library): reduce dependecies on old code, simplify normalize module
|
2016-09-19 22:12:34 -07:00 |
|
equations.h
|
chore(library/equations_compiler/equations): style
|
2016-09-23 10:05:18 -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
|
|
|
|
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_rec): bug in decoder
|
2016-12-18 22:51:02 -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
|
fix(frontends/lean/pp,library/equations_compiler,library/tactic/smt/congruence_closure): bug at to_char function
|
2017-01-11 23:44:25 -08:00 |
|
util.h
|
feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names
|
2017-01-06 11:40:34 -08:00 |
