lean4-htt/src/util
Sebastian Ullrich 30e23eae2b
perf: avoid allocation on lean_trace use in interpreter (#12036)
After #12001, it was no longer true that `lean_trace(name(...), ...)`
would only perform the name allocation if no trace option was set. This
PR instead avoids the allocation in any case by avoiding this pattern.
2026-01-18 19:33:48 +00:00
..
alloc.h perf: use mimalloc with important C++ hash maps (#7868) 2025-04-11 16:23:33 +00:00
ascii.cpp
ascii.h
bit_tricks.cpp
bit_tricks.h
CMakeLists.txt fix: Windows needs more LEAN_EXPORTs 2024-08-12 14:14:42 +02:00
escaped.cpp
escaped.h
exception_with_pos.h
ffi.cpp chore: CMAKE_CXX_SYSROOT_FLAG is also needed for linking (#6297) 2024-12-03 16:14:22 +00:00
freset.h
init_module.cpp fix: Windows needs more LEAN_EXPORTs 2024-08-12 14:14:42 +02:00
init_module.h fix: Windows needs more LEAN_EXPORTs 2024-08-12 14:14:42 +02:00
io.h feat: zero cost BaseIO (#10625) 2025-10-22 10:55:12 +02:00
kvmap.cpp feat: implement bool operator==(data_value const & a, data_value const & b) using Lean autogenerated code 2021-12-16 16:37:47 -08:00
kvmap.h perf: mark move constructors and assignment operators as noexcept (#10784) 2025-10-22 14:21:51 +00:00
lbool.cpp
lbool.h
list.h perf: mark move constructors and assignment operators as noexcept (#10784) 2025-10-22 14:21:51 +00:00
list_fn.cpp
list_fn.h
macros.h
map_foreach.cpp fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
map_foreach.h
message_definitions.h feat: define Int8 (#5790) 2024-10-25 06:06:40 +00:00
name.cpp fix: Windows needs more LEAN_EXPORTs 2024-08-12 14:14:42 +02:00
name.h perf: mark move constructors and assignment operators as noexcept (#10784) 2025-10-22 14:21:51 +00:00
name_generator.cpp
name_generator.h
name_hash_map.h perf: used hashmaps for symbol lookup in the interpreter (#10927) 2025-10-23 11:45:20 +00:00
name_hash_set.h perf: use lean::unordered_map/set everywhere (#11957) 2026-01-12 17:14:09 +00:00
name_map.h
name_set.cpp
name_set.h
nat.h perf: mark move constructors and assignment operators as noexcept (#10784) 2025-10-22 14:21:51 +00:00
null_ostream.h
option_declarations.cpp feat: document that backward options may disappear (#11304) 2025-11-24 17:49:46 +00:00
option_declarations.h fix: Windows needs more LEAN_EXPORTs 2024-08-12 14:14:42 +02:00
options.cpp perf: avoid allocation on lean_trace use in interpreter (#12036) 2026-01-18 19:33:48 +00:00
options.h perf: Options.hasTrace (#12001) 2026-01-16 09:03:40 +00:00
output_channel.h chore: fix spelling mistakes in non-Lean files (#5430) 2024-09-23 21:11:20 +00:00
pair.h
path.cpp fix: resolve symbolic links through IO.FS.realPath on windows (#8534) 2025-06-13 13:16:13 +00:00
path.h fix: resolve symbolic links through IO.FS.realPath on windows (#8534) 2025-06-13 13:16:13 +00:00
rb_map.h
rb_tree.h perf: mark move constructors and assignment operators as noexcept (#10784) 2025-10-22 14:21:51 +00:00
rc.h
shell.cpp refactor: port shell option processing to Lean (v2) (#11434) 2025-12-02 17:41:51 +00:00
test.h
timeit.cpp
timeit.h chore: fix C++ warning (#10922) 2025-10-24 11:09:08 +00:00
timer.cpp
timer.h
unit.h
unlock_guard.h