Leonardo de Moura 9564758965 refactor(library/definitional/no_confusion): use new type_checker to derive no_confusion		2016-03-21 15:40:58 -07:00
..
brec_on.cpp	refactor(library/definitional): use new type_checker	2016-03-21 15:01:29 -07:00
brec_on.h
cases_on.cpp	refactor(library/definitional): use new type_checker	2016-03-21 15:01:29 -07:00
cases_on.h
CMakeLists.txt	feat(CMakeLists): add shared library	2015-08-13 11:21:05 -07:00
equations.cpp	refactor(library/util): isolate util procedures that depend on old_type_checker	2016-03-21 13:36:08 -07:00
equations.h	refactor(library): create copy of the kernel type_checker in library	2016-03-18 14:34:10 -07:00
induction_on.cpp	feat(library,library/definitional): tag auxiliary recursors automatically generated by Lean	2015-09-11 10:08:54 -07:00
induction_on.h
init_module.cpp	refactor(library/util): isolate util procedures that depend on old_type_checker	2016-03-21 13:36:08 -07:00
init_module.h
no_confusion.cpp	refactor(library/definitional/no_confusion): use new type_checker to derive no_confusion	2016-03-21 15:40:58 -07:00
no_confusion.h
projection.cpp	refactor(kernel): remove extension_context	2016-03-19 15:15:39 -07:00
projection.h	feat(library/definitional/projection): define projections using auxiliary macro	2015-07-02 10:49:49 -07:00
rec_on.cpp	refactor(*): remove name_generator and use simpler mk_fresh_name	2016-02-11 18:05:57 -08:00
rec_on.h