def same_dimensions
bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:96
import bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend as GradientPROOF
import Base
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwiseProof
96def same_dimensions(-original: Core.Dynamic, -retained: Core.Dynamic, -same: Totality.SameSource(original, retained)) ->
97 Holds<{Totality.dimensions(retained) == Totality.dimensions(original) : List<&2, U32>}>:
98 Holds{Equal.cong(Totality.Inspection, List<&2, U32>, ElementwiseProof.inspection_dimensions,
99 Totality.inspect(Totality.Dimensions{}, retained), Totality.inspect(Totality.Dimensions{}, original), same(Totality.Dimensions{}))}