def digits_offset
bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1735
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as ShapeIndex
1735def digits_offset(+dimensions: List<&2, Nat>, +values: List<&2, Nat>, +fits: Coordinates.Fits(dimensions, values)) ->
1736 {Shape.digits(dimensions, Shape.offset(dimensions, values)) == values : List<&2, Nat>}:
1737 %Equal.trans(Nat, Shape.Fin.value(Shape.numel(dimensions), Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits))),
1738 Shape.row_major(dimensions, Coordinates.coordinate_of(dimensions, values, fits)), Shape.offset(dimensions, values),
1739 ShapeIndex.flatten_row_major(dimensions, Coordinates.coordinate_of(dimensions, values, fits)), Coordinates.offset_of(dimensions, values, fits)) :
1740 {Shape.digits(dimensions, _) == values : List<&2, Nat>}
1741 Equal.trans(List<&2, Nat>,
1742 Shape.digits(dimensions, Shape.Fin.value(Shape.numel(dimensions), Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits)))),
1743 Shape.indices(dimensions, Shape.unflatten(dimensions, Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits)))), values,
1744 Equal.sym(List<&2, Nat>,
1745 Shape.indices(dimensions, Shape.unflatten(dimensions, Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits)))),
1746 Shape.digits(dimensions, Shape.Fin.value(Shape.numel(dimensions), Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits)))),
1747 Coordinates.digits_unflatten(dimensions, Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits)))),
1748 Equal.trans(List<&2, Nat>,
1749 Shape.indices(dimensions, Shape.unflatten(dimensions, Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits)))),
1750 Shape.indices(dimensions, Coordinates.coordinate_of(dimensions, values, fits)), values,
1751 Equal.cong(Shape.Coordinate(dimensions), List<&2, Nat>, Shape.indices(dimensions),
1752 Shape.unflatten(dimensions, Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits))),
1753 Coordinates.coordinate_of(dimensions, values, fits), ShapeIndex.unflatten_flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits))),
1754 Coordinates.indices_of(dimensions, values, fits)))