Rob23oba 6bec8adf16 fix: symbol name for native boxed declarations in the interpreter (#12095) ... This PR fixes the procedure for finding the mangled symbol name of boxed variants of native functions. Previously, the wrong symbol name has been used for names ending in `_`: For example `test_` mangles to `l_test__` but `test_._boxed` mangles to `l_test___00__boxed`, not `l_test_____boxed` which the compiler would previously wrongly use. This probably didn't affect anybody though since the failure condition is pretty rare: the name of a native function that the interpreter tries to execute would've had to end in `_`.		2026-01-21 20:38:29 +00:00
..
constructions	perf: do not consult isNoConfusion in whnf (#11571)	2025-12-09 23:36:46 +00:00
annotation.cpp
annotation.h	chore: fix more typos in comments	2023-10-08 14:37:34 -07:00
bin_app.cpp
bin_app.h
class.cpp	feat: split Lean.Kernel.Environment from Lean.Environment (#5145)	2025-01-18 18:42:57 +00:00
class.h	feat: split Lean.Kernel.Environment from Lean.Environment (#5145)	2025-01-18 18:42:57 +00:00
CMakeLists.txt	perf: do not consult isNoConfusion in whnf (#11571)	2025-12-09 23:36:46 +00:00
constants.cpp	feat: add support for Float32 to the Lean runtime (#6348)	2024-12-09 21:33:43 +00:00
constants.h	feat: add support for Float32 to the Lean runtime (#6348)	2024-12-09 21:33:43 +00:00
constants.txt	feat: add support for Float32 to the Lean runtime (#6348)	2024-12-09 21:33:43 +00:00
dynlib.cpp	feat: zero cost BaseIO (#10625)	2025-10-22 10:55:12 +02:00
dynlib.h	feat: smarter plugin loading (#7090)	2025-02-18 23:03:52 +00:00
elab_environment.cpp	refactor: port shell option processing to Lean (v2) (#11434)	2025-12-02 17:41:51 +00:00
elab_environment.h	perf: mark move constructors and assignment operators as noexcept (#10784)	2025-10-22 14:21:51 +00:00
expr_lt.cpp	feat: add the nondep field of Expr.letE to the C++ data model (#8751)	2025-06-14 23:10:27 +00:00
expr_lt.h
expr_pair.h
expr_pair_maps.h	perf: use lean::unordered_map/set everywhere (#11957)	2026-01-12 17:14:09 +00:00
expr_unsigned_map.h	perf: use lean::unordered_map/set everywhere (#11957)	2026-01-12 17:14:09 +00:00
formatter.cpp
formatter.h
init_attribute.cpp	chore: move the IR interpreter from library/compiler to library (#9265)	2025-07-08 20:45:55 +00:00
init_attribute.h	chore: move the IR interpreter from library/compiler to library (#9265)	2025-07-08 20:45:55 +00:00
init_module.cpp	chore: move the IR interpreter from library/compiler to library (#9265)	2025-07-08 20:45:55 +00:00
init_module.h	fix: Windows needs more LEAN_EXPORTs	2024-08-12 14:14:42 +02:00
ir_interpreter.cpp	fix: symbol name for native boxed declarations in the interpreter (#12095)	2026-01-21 20:38:29 +00:00
ir_interpreter.h	chore: move the IR interpreter from library/compiler to library (#9265)	2025-07-08 20:45:55 +00:00
ir_types.h	feat: zero cost BaseIO (#10625)	2025-10-22 10:55:12 +02:00
llvm.cpp	feat: zero cost BaseIO (#10625)	2025-10-22 10:55:12 +02:00
max_sharing.cpp	perf: use lean::unordered_map/set everywhere (#11957)	2026-01-12 17:14:09 +00:00
max_sharing.h
module.cpp	perf: avoid double-open per .olean file (#11507)	2025-12-05 09:37:38 +00:00
module.h	feat: split Lean.Kernel.Environment from Lean.Environment (#5145)	2025-01-18 18:42:57 +00:00
num.cpp
num.h
print.cpp	feat: add the nondep field of Expr.letE to the C++ data model (#8751)	2025-06-14 23:10:27 +00:00
print.h	fix: Windows needs more LEAN_EXPORTs	2024-08-12 14:14:42 +02:00
profiling.cpp
profiling.h	fix: Windows needs more LEAN_EXPORTs	2024-08-12 14:14:42 +02:00
reducible.cpp	feat: split Lean.Kernel.Environment from Lean.Environment (#5145)	2025-01-18 18:42:57 +00:00
reducible.h	feat: split Lean.Kernel.Environment from Lean.Environment (#5145)	2025-01-18 18:42:57 +00:00
replace_visitor.cpp
replace_visitor.h
suffixes.h	fix: allow arbitrary sorts in structural recursion over reflexive inductive types (#7639)	2025-06-13 21:51:09 +00:00
time_task.cpp	feat: zero cost BaseIO (#10625)	2025-10-22 10:55:12 +02:00
time_task.h	perf: remove most remaining async blockers in Init.Data.List.Sublist (#7500)	2025-03-15 15:26:06 +00:00
util.cpp	chore: delete obsolete C++ file (#11561)	2025-12-09 15:47:54 +00:00
util.h	refactor: remove unnecessary export attributes (#9281)	2025-07-09 16:55:00 +00:00