The Lean Language Reference

21.1. Boxing🔗

Lean values may be represented at runtime in two ways:

  • Boxed values may be pointers to heap values or require shifting and masking.

  • Unboxed values are immediately available.

Boxed values are either a pointer to an object, in which case the lowest-order bit is 0, or an immediate value, in which case the lowest-order bit is 1 and the value is found by shifting the representation to the right by one bit.

Types with an unboxed representation, such as UInt8 and enum inductive types, are represented as the corresponding C types in contexts where the compiler can be sure that the value has said type. In some contexts, such as generic container types like Array, otherwise-unboxed values must be boxed prior to storage. In other words, Bool.not is called with and returns unboxed uint8_t values because the enum inductive type Bool has an unboxed representation, but the individual Bool values in an Array Bool are boxed. A field of type Bool in an inductive type's constructor is represented unboxed, while Bools stored in polymorphic fields that are instantiated as Bool are boxed.