Leonardo de Moura 6f95f4668f fix(library/inductive_compiler/ginductive): constructors of mutually inductive datatypes were not being registered ... Actually, the constructors of the first inductive datatype in a mutually recursive definitions were being registered.		2017-02-04 18:51:17 -08:00
..
add_decl.cpp	fix(inductive_compiler): generate has_sizeof for structures	2016-10-05 15:10:21 -07:00
add_decl.h	feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class	2016-09-29 17:56:35 -07:00
basic.cpp	chore(library): poly_unit ==> punit	2017-01-30 11:54:00 -08:00
basic.h	feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class	2016-09-29 17:56:35 -07:00
CMakeLists.txt	feat(src/library/inductive_compiler): support for nested inductive types	2016-09-16 12:50:59 -07:00
compiler.cpp	feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class	2016-09-29 17:56:35 -07:00
compiler.h	feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class	2016-09-29 17:56:35 -07:00
ginductive.cpp	fix(library/inductive_compiler/ginductive): constructors of mutually inductive datatypes were not being registered	2017-02-04 18:51:17 -08:00
ginductive.h	feat(src/library/inductive_compiler): support for nested inductive types	2016-09-16 12:50:59 -07:00
ginductive_decl.cpp	feat(src/library/inductive_compiler): support for nested inductive types	2016-09-16 12:50:59 -07:00
ginductive_decl.h	feat(src/library/inductive_compiler): support for nested inductive types	2016-09-16 12:50:59 -07:00
init_module.cpp	feat(src/library/inductive_compiler): support for nested inductive types	2016-09-16 12:50:59 -07:00
init_module.h
mutual.cpp	chore(library): poly_unit ==> punit	2017-01-30 11:54:00 -08:00
mutual.h	feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class	2016-09-29 17:56:35 -07:00
nested.cpp	refactor(library/tactic): move defeq_canonizer::state to tactic_state	2017-01-07 10:17:51 -08:00
nested.h	feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class	2016-09-29 17:56:35 -07:00
util.cpp	fix(library/inductive_compiler/util): allow untrusted/meta declarations when checking intermediate steps	2016-11-13 12:32:49 -08:00
util.h	feat(src/library/inductive_compiler): support for nested inductive types	2016-09-16 12:50:59 -07:00