Module claim_fold 

Proving a fold of evaluation claims on one sparse tensor.

Structs

AxisClaim

An evaluation claim whose point is cut into one run per tensor axis.

Functions

claim_at

Builds a claim asserting the tensor’s extension takes the value it actually takes.

evaluate

The tensor’s multilinear extension at one point, evaluated directly from its entries.

prove

Proves a fold of evaluation claims on one tensor, returning the claim they folded to.

split_axes

Cuts a flat point into one run per axis, lowest axis first.

Type Aliases

TensorEntry

One nonzero of a sparse tensor: a flat index over every axis, and the value carried there.