LEAN_SMALL_ALLOCATOR

Stream: lean4 dev

[Chase Norman]

Generally, when should we expect LEAN_SMALL_ALLOCATOR to be defined? Also, why are all of these functions in lean/lean.h declared inline? Especially for those with dependencies on a compile-time parameter like LEAN_SMALL_ALLOCATOR, it is important that these symbols are exported so that external programs can be assured that they are using the correct implementation.

[Henrik Böving]

Generally, when should we expect LEAN_SMALL_ALLOCATOR to be defined?

Always unless the user is using a non default build

Also, why are all of these functions in lean/lean.h declared inline

For performance reasons, a normal Lean program pretty much doesn't do anything else apart from calling functions from lean.h

[Chase Norman]

Thanks!