Leonardo de Moura f5fd962a25 feat: safe exponentiation (#4637) ... Summary: - Adds configuration option `exponentiation.threshold` - An expression `b^n` where `b` and `n` are literals is not reduced by `whnf`, `simp`, and `isDefEq` if `n > exponentiation.threshold`. Motivation: prevents system from becoming irresponsive and/or crashing without memory. TODO: improve support in the kernel. It is using a hard-coded limit for now.		2024-07-03 05:12:53 +00:00
..
abstract.cpp	feat: generalize Expr.abstractRange	2022-03-08 18:19:17 -08:00
abstract.h	chore: remove Expr.localE constructor	2020-11-01 09:37:48 -08:00
cache_stack.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
CMakeLists.txt	chore: move trace.cpp to kernel (#4014)	2024-04-28 17:24:48 +00:00
declaration.cpp	fix: mismatch between TheoremVal in Lean and C++ (#4035)	2024-04-30 18:10:20 +00:00
declaration.h	fix: mismatch between TheoremVal in Lean and C++ (#4035)	2024-04-30 18:10:20 +00:00
environment.cpp	fix: adapt kernel interruption to new cancellation system (#4584)	2024-07-01 14:52:42 +00:00
environment.h	feat: collect kernel diagnostic information (#4082)	2024-05-06 21:53:16 +00:00
equiv_manager.cpp	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
equiv_manager.h	chore(*): rename expr_struct_* to expr_*	2018-04-09 12:55:48 -07:00
expr.cpp	perf: implement Expr.update* in Lean	2022-07-19 05:55:13 -07:00
expr.h	chore: remove remnants of C++ format	2022-11-18 06:11:24 -08:00
expr_cache.cpp	refactor(kernel/expr): implement expr using runtime/object	2018-06-21 16:05:33 -07:00
expr_cache.h
expr_eq_fn.cpp	fix: switch to C++ interruption whitelist	2023-10-26 08:33:09 +02:00
expr_eq_fn.h	feat(library/type_context): allow us to control whether binder information is taken into account or not when caching type information	2016-08-01 16:34:07 -07:00
expr_maps.h	chore(*): rename expr_struct_* to expr_*	2018-04-09 12:55:48 -07:00
expr_sets.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
find_fn.h
for_each_fn.cpp	fix: remove unguarded check_interrupted call	2023-10-26 08:33:09 +02:00
for_each_fn.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
inductive.cpp	feat: collect kernel diagnostic information (#4082)	2024-05-06 21:53:16 +00:00
inductive.h	fix: do not apply eta for structures in Prop	2022-03-01 09:00:46 -08:00
init_module.cpp	chore: move trace.cpp to kernel (#4014)	2024-04-28 17:24:48 +00:00
init_module.h
instantiate.cpp	refactor: instantiateTypeLevelParams in Lean	2022-10-24 12:23:13 -07:00
instantiate.h	chore: remove instance cache	2020-07-08 09:40:34 -07:00
kernel_exception.h	feat: type of theorems must be propositions	2024-03-13 12:37:58 -07:00
level.cpp	chore: remove remnants of C++ format	2022-11-18 06:11:24 -08:00
level.h	chore: fix more typos in comments	2023-10-08 14:37:34 -07:00
local_ctx.cpp	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
local_ctx.h	fix: nonoptimal specialization	2020-09-24 12:40:28 -07:00
quot.cpp	fix: binder name	2021-08-26 11:11:37 -07:00
quot.h	fix: quot reduction bug	2023-10-11 21:25:34 -07:00
replace_fn.cpp	fix: switch to C++ interruption whitelist	2023-10-26 08:33:09 +02:00
replace_fn.h	chore: reduce src/include/lean	2021-09-07 08:24:54 -07:00
trace.cpp	chore: move trace.cpp to kernel (#4014)	2024-04-28 17:24:48 +00:00
trace.h	chore: move trace.cpp to kernel (#4014)	2024-04-28 17:24:48 +00:00
type_checker.cpp	feat: safe exponentiation (#4637)	2024-07-03 05:12:53 +00:00
type_checker.h	feat: safe exponentiation (#4637)	2024-07-03 05:12:53 +00:00