Certified einsum operand views #
This module composes an optimized einsum operand index with a certified flat input view. Generated code reads the original source tensor directly, while the returned equality still targets the logical operand stored in the independent einsum semantics.
def
TorchLean.Tensor.Internal.Elab.Impl.compileInputViewRead
(logicalTensor logicalSize inputIndexValue normalizedInputIndexValue certifiedInputIndex hInputIndexValue : Lean.Expr)
(useNativeLogicalIndex : Bool)
(view? : Option (Lean.Expr × Lean.Expr × Lean.Expr))
:
Compile one logical operand read, optionally through a certified source view.
The optional tuple contains the source tensor, its logical-input-to-source flat map, and the pointwise theorem that source reads equal reads from the logical operand.