Pack reports

This module reports segment metadata and native execution for concrete pack and unpack certificates.

Unpack returns a component-indexed function. Its reported total counts describe evaluating each component once; they do not imply that all component buffers are allocated eagerly.

def TorchLean.Tensor.Internal.Report.Impl.concretePackReport (operation : String) (checked scalarType : Lean.Expr) : Lean.MetaM (Option String)

Decode concrete pack or unpack metadata into its segment-level report.