def axis_term
bendtorch-core@0.1.0.0 · src/shape/projection_proofs.bend:94
import bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend as ProjectionProofs
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
94def axis_term(+size: Nat, +stride: Nat, +value: Nat) -> {Nat.mul(Shape.broadcast_index(size, stride), value) == Nat.mul(Shape.broadcast_index(size, value), stride) : Nat}:
95 match size:
96 case 0n:
97 Nats.mul_comm(stride, value)
98 case 1n+p:
99 match p:
100 case 0n:
101 {==}
102 case 1n+q:
103 Nats.mul_comm(stride, value)