f47dfe9e7f
Drastically speeds up `isTracingEnabledFor` in the common case, which has evolved from "no options set" to "`Elab.async` and probably some linter options set but no `trace`". ## Breaking changes `Lean.Options` is now an opaque type. The basic but not all of the `KVMap` API has been redefined on top of it. |
||
|---|---|---|
| .. | ||
| abstract.cpp | ||
| abstract.h | ||
| CMakeLists.txt | ||
| declaration.cpp | ||
| declaration.h | ||
| environment.cpp | ||
| environment.h | ||
| equiv_manager.cpp | ||
| equiv_manager.h | ||
| expr.cpp | ||
| expr.h | ||
| expr_cache.cpp | ||
| expr_cache.h | ||
| expr_eq_fn.cpp | ||
| expr_eq_fn.h | ||
| expr_maps.h | ||
| expr_sets.h | ||
| find_fn.h | ||
| for_each_fn.cpp | ||
| for_each_fn.h | ||
| inductive.cpp | ||
| inductive.h | ||
| init_module.cpp | ||
| init_module.h | ||
| instantiate.cpp | ||
| instantiate.h | ||
| instantiate_mvars.cpp | ||
| kernel_exception.h | ||
| level.cpp | ||
| level.h | ||
| local_ctx.cpp | ||
| local_ctx.h | ||
| quot.cpp | ||
| quot.h | ||
| replace_fn.cpp | ||
| replace_fn.h | ||
| trace.cpp | ||
| trace.h | ||
| type_checker.cpp | ||
| type_checker.h | ||