def reshape_decision_success

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1352

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as Mapping

1352def reshape_decision_success(+input: Shape.Shape, +target: Shape.Shape,
1353  decision: Shape.BoolCase<Nat.is_eq(Shape.elements(input), Shape.elements(target))>, source: Core.Tensor<input>,
1354  -same: {Shape.elements(input) == Shape.elements(target) : Nat}) -> ReshapeDecisionSuccess<input, target, source, decision>:
1355  match decision:
1356    case Shape.BFalse{equal}:
1357      ReshapeDecisionSuccess{Empty.absurd({Result.is_done(&2, &1, Transforms.Error, Core.Dynamic,
1358        Transforms.reshape_decided(input, target, source, Shape.BFalse{equal})) == True{} : Bool},
1359        Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.elements(input), Shape.elements(target)), True{}, equal,
1360          Mapping.natural_equal_true(Shape.elements(input), Shape.elements(target), same))))}
1361    case Shape.BTrue{equal}:
1362      ReshapeDecisionSuccess{{==}}