| .. |
|
CMakeLists.txt
|
feat(library/equations_compiler): add pack_mutual
|
2017-05-18 15:29:51 -07:00 |
|
compiler.cpp
|
feat(library/equations_compiler): add wf_rec skeleton
|
2017-05-17 12:47: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
|
fix(library/equations_compiler/elim_match): handle partially applied constructors
|
2017-05-22 17:17:27 +02:00 |
|
elim_match.h
|
feat(library/equations_compiler): add mk_nonrec
|
2016-09-08 14:09:05 -07:00 |
|
equations.cpp
|
feat(frontends/lean,library/equations_compiler): store tactics for generating well founded relation and decreasing proofs
|
2017-05-23 15:00:29 -07:00 |
|
equations.h
|
feat(frontends/lean,library/equations_compiler): store tactics for generating well founded relation and decreasing proofs
|
2017-05-23 15:00:29 -07:00 |
|
init_module.cpp
|
feat(library/equations_compiler): add pack_mutual
|
2017-05-18 15:29:51 -07:00 |
|
init_module.h
|
|
|
|
pack_domain.cpp
|
feat(library/equations_compiler): invoke tactics for building well founded relation, and proving recursive calls are "decreasing"
|
2017-05-23 16:04:55 -07:00 |
|
pack_domain.h
|
refactor(library/equations_compiler): move pack_domain to new module
|
2016-08-15 08:22:23 -07:00 |
|
pack_mutual.cpp
|
feat(library/equations_compiler): invoke tactics for building well founded relation, and proving recursive calls are "decreasing"
|
2017-05-23 16:04:55 -07:00 |
|
pack_mutual.h
|
feat(library/equations_compiler): unpack auxiliary definition
|
2017-05-20 20:34:18 -07:00 |
|
structural_rec.cpp
|
fix(library/equations_compiler/structural_rec): fix indices
|
2017-05-07 15:52:39 +02:00 |
|
structural_rec.h
|
chore(library/equations_compiler/structural_rec): update comment
|
2017-03-05 11:03:36 -08: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
|
feat(library/equations_compiler): prove equational lemmas for auxiliary definition
|
2017-05-20 16:38:32 -07:00 |
|
util.h
|
feat(library/equations_compiler): add pack_mutual
|
2017-05-18 15:29:51 -07:00 |
|
wf_rec.cpp
|
feat(library/init): use Sort instead of Type for defining acc and well_founded
|
2017-05-23 16:40:45 -07:00 |
|
wf_rec.h
|
feat(library/equations_compiler): add wf_rec skeleton
|
2017-05-17 12:47:52 -07:00 |
