| .. |
|
CMakeLists.txt
|
feat(library/equations_compiler): add elim_match skeleton
|
2016-08-17 21:38:23 -07:00 |
|
compiler.cpp
|
fix(library/equations_compiler/compiler): nested match-exprs in meta_definitions
|
2016-09-18 17:20:52 -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): do not create auxiliary definition when compiling meta-definitions and/or lemmas
|
2016-09-12 12:54:01 -07: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 mk_nonrec
|
2016-09-08 14:09:05 -07:00 |
|
equations.h
|
feat(library/equations_compiler/equations): add helper function
|
2016-09-09 17:43:42 -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
|
|
|
|
old_compiler.cpp
|
chore(kernel): remove support for mutually inductive datatypes from the kernel
|
2016-09-10 17:39:17 -07:00 |
|
old_compiler.h
|
|
|
|
old_goal.cpp
|
|
|
|
old_goal.h
|
|
|
|
old_inversion.cpp
|
|
|
|
old_inversion.h
|
|
|
|
pack_domain.cpp
|
fix(library/equations_compiler/pack_domain): missing case
|
2016-09-09 13:39:51 -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 at check_arg_type
|
2016-09-18 18:36:20 -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 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(library/tactic/defeq_simplifier): move defeq_simp_lemmas to library
|
2016-09-12 10:36:11 -07:00 |
|
util.h
|
feat(library/equations_compiler): add option eqn_compiler.zeta
|
2016-09-10 14:00:16 -07:00 |
