Zulip Chat Archive
Stream: lean4
Topic: Introduce `m_foreach_allocation` to `lean_extern_object`
Schrodinger ZHU Yifan (Sep 03 2023 at 02:16):
I think this might be a minor point but it may be helpful if we have a cleaner leak sanitizer report when using external objects?
https://github.com/leanprover/lean4/issues/2507
Last updated: Dec 20 2023 at 11:08 UTC