TransformPROOF.reshape_decision_success: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
Lines 1352-1362 of bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&start_line=1352&end_line=1362

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

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

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.is_done
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=elements
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend&name=natural_equal_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=ReshapeDecisionSuccess
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=reshape_decided