Leonardo de Moura 7945b8adab refactor(kernel/type_checker): remove useless procedures		2015-02-07 14:55:36 -08:00
..
inductive	fix(kernel/inductive/inductive): fix assertion violation when K is applied to type incorrect term	2015-01-27 11:22:14 -08:00
abstract.cpp	feat(kernel/abstract): add new abstract_local procedure	2014-12-20 11:31:48 -08:00
abstract.h	feat(kernel/abstract): add new abstract_local procedure	2014-12-20 11:31:48 -08:00
cache_stack.h	perf(kernel/for_each_fn): use cache stack trick at for_each_fn	2014-07-23 19:32:11 -07:00
CMakeLists.txt	refactor(kernel): move default_converter to its own module	2015-02-07 11:33:37 -08:00
constraint.cpp	fix(kernel/constraint): bug in operator<<	2014-10-14 15:22:03 -07:00
constraint.h	feat(library/unifier): add 'on-demand' choice constraints, they are processed as soon as their type does not contain meta-variables anymore	2014-09-27 21:50:39 -07:00
converter.cpp	refactor(kernel): move default_converter to its own module	2015-02-07 11:33:37 -08:00
converter.h	feat(frontends/lean): default 'eval' command ignores opaque/irreducible annotations	2014-11-10 12:46:04 -08:00
declaration.cpp	refactor(*): add method get_num_univ_params	2015-01-28 17:22:18 -08:00
declaration.h	refactor(*): add method get_num_univ_params	2015-01-28 17:22:18 -08:00
default_converter.cpp	refactor(kernel/default_converter): avoid carrying type_checker and delayed_justification around in the default_converter	2015-02-07 14:10:56 -08:00
default_converter.h	refactor(kernel/default_converter): avoid carrying type_checker and delayed_justification around in the default_converter	2015-02-07 14:10:56 -08:00
environment.cpp	refactor(*): explicit initialization/finalization for environment extensions	2014-09-22 17:30:29 -07:00
environment.h	refactor(kernel/type_checker): remove useless procedures	2015-02-07 14:55:36 -08:00
error_msgs.cpp	perf(kernel/error_msgs): avoid unnecessary work	2015-01-15 18:32:52 -08:00
error_msgs.h	feat(kernel/error_msgs): improve application type mismatch error messages	2014-07-28 07:08:12 -07:00
expr.cpp	feat(kernel/expr): change the rules for inferring implicit arguments, closes #344	2014-11-25 12:54:07 -08:00
expr.h	feat(kernel/type_checker): add is_stuck method, and improve ensure_pi method, closes #261	2014-10-27 13:16:50 -07:00
expr_cache.cpp	refactor(kernel): add expr_cache	2015-02-03 14:59:55 -08:00
expr_cache.h	refactor(kernel): add expr_cache	2015-02-03 14:59:55 -08:00
expr_eq_fn.cpp	perf(kernel/expr_eq_fn): use thread local cache, and avoid memory allocation/deallocation	2014-10-17 16:44:20 -07:00
expr_eq_fn.h	perf(kernel/expr_eq_fn): use thread local cache, and avoid memory allocation/deallocation	2014-10-17 16:44:20 -07:00
expr_maps.h	refactor(kernel/expr): remove dead code	2014-10-16 13:09:26 -07:00
expr_sets.h	perf(kernel/expr_eq_fn): use thread local cache, and avoid memory allocation/deallocation	2014-10-17 16:44:20 -07:00
extension_context.cpp	feat(kernel/extension_context): add auxiliary method is_def_eq	2015-01-27 11:17:54 -08:00
extension_context.h	feat(kernel/extension_context): add auxiliary method is_def_eq	2015-01-27 11:17:54 -08:00
find_fn.h	refactor(kernel/find_fn): simplify find_fn module	2014-07-23 18:09:58 -07:00
for_each_fn.cpp	feat(kernel): add memory consumption checks at replace_fn and for_each_fn	2015-01-15 16:54:55 -08:00
for_each_fn.h	refactor(kernel/for_each_fn): simplify module interface	2014-07-23 18:16:41 -07:00
formatter.cpp	refactor(kernel): explicit initialization/finalization	2014-09-24 10:12:28 -07:00
formatter.h	refactor(kernel): explicit initialization/finalization	2014-09-24 10:12:28 -07:00
free_vars.cpp	perf(kernel/free_vars): improve has_free_var	2015-01-15 18:42:56 -08:00
free_vars.h	refactor(kernel/expr): remove dead code	2014-10-16 13:09:26 -07:00
init_module.cpp	refactor(kernel): move default_converter to its own module	2015-02-07 11:33:37 -08:00
init_module.h	refactor(*): explicit initialization/finalization for serialization	2014-09-22 15:26:41 -07:00
instantiate.cpp	refactor(*): add method get_num_univ_params	2015-01-28 17:22:18 -08:00
instantiate.h	refactor(*): add method get_num_univ_params	2015-01-28 17:22:18 -08:00
justification.cpp	refactor(*): remove dependency to thread_local C++11 keyword, the	2014-09-24 12:51:04 -07:00
justification.h	refactor(kernel/formatter): add formatter_factory, and simplify formatter interface	2014-07-10 18:32:00 +01:00
kernel_exception.cpp	feat(*): distinguish between logical and runtime exceptions.	2015-01-15 16:54:55 -08:00
kernel_exception.h	feat(*): distinguish between logical and runtime exceptions.	2015-01-15 16:54:55 -08:00
level.cpp	perf(kernel/level): apply two simple normalization rules at mk_max	2014-11-16 18:16:57 -08:00
level.h	feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2)	2014-11-12 17:28:33 -08:00
metavar.cpp	refactor(kernel): add expr_cache	2015-02-03 14:59:55 -08:00
metavar.h	fix(frontends/lean/elaborator): unsolved metavariables, fix #329	2014-11-26 11:56:39 -08:00
normalizer_extension.cpp	feat(kernel/type_checker): add is_stuck method, and improve ensure_pi method, closes #261	2014-10-27 13:16:50 -07:00
normalizer_extension.h	feat(kernel/type_checker): add is_stuck method, and improve ensure_pi method, closes #261	2014-10-27 13:16:50 -07:00
pos_info_provider.cpp	refactor(*): use + for concatenating format objects	2014-08-24 09:35:25 -07:00
pos_info_provider.h	chore(*): create alias for std::pair	2014-08-20 16:46:19 -07:00
replace_fn.cpp	feat(kernel/replace_fn): add use_cache flag to replace function	2015-02-05 10:49:18 -08:00
replace_fn.h	feat(kernel/replace_fn): add use_cache flag to replace function	2015-02-05 10:49:18 -08:00
type_checker.cpp	refactor(kernel/type_checker): remove useless procedures	2015-02-07 14:55:36 -08:00
type_checker.h	refactor(kernel/type_checker): remove useless procedures	2015-02-07 14:55:36 -08:00