def same_dimensions

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:82

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

82def same_dimensions(-original: Core.Dynamic, -retained: Core.Dynamic, -same: Totality.SameSource(original, retained)) ->
83  Holds<{Totality.dimensions(retained) == Totality.dimensions(original) : List<&2, U32>}>:
84  Holds{Equal.cong(Totality.Inspection, List<&2, U32>, ElementwiseProof.inspection_dimensions,
85    Totality.inspect(Totality.Dimensions{}, retained), Totality.inspect(Totality.Dimensions{}, original), same(Totality.Dimensions{}))}