TransformPROOF.reshape_built_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 1369-1390 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=1369&end_line=1390 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/shape/LAWS.bend as ShapeLaws import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as Mapping def reshape_built_success(+input: Shape.Shape, +target: Shape.Shape, built: Shape.ConstructResult, source: Core.Tensor, -same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}, -complete: {ShapeLaws.built(Shape.dimensions(target), built) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>}) -> ReshapeBuiltSuccess: match built: case Shape.SError{error}: ReshapeBuiltSuccess{Empty.absurd({Result.is_done(&2, &1, Transforms.Error, Core.Dynamic, Transforms.reshape_built(input, source, Shape.dimensions(target), Shape.SError{error})) == True{} : Bool}, Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, Mapping.metadata_present, None{}, Some{Shape.dimensions(target)}, complete)))} case Shape.SBuilt{+output, preserved}: ReshapeBuiltSuccess{ {\{ReshapeDecisionSuccess: success => success} : ReshapeDecisionSuccess -> {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic, Transforms.reshape_decided(input, output, source, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output))))) == True{} : Bool}}( reshape_decision_success(input, output, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output))), source, Mapping.element_counts_same(input, output, Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target)), Shape.logical_numel(Shape.dimensions(output)), same, Equal.cong(List<&2, U32>, Nat, Shape.logical_numel, Shape.dimensions(target), Shape.dimensions(output), Equal.sym(List<&2, U32>, Shape.dimensions(output), Shape.dimensions(target), preserved))))))} Uses (29): 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.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe 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=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=built https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=ConstructResult 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=bool_case https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions 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/shape/core.bend&name=logical_numel 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=element_counts_same https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend&name=metadata_present https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=ReshapeBuiltSuccess 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/transform_PROOF.bend&name=reshape_decision_success 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_built https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=reshape_decided