TransformPROOF.actual_advanced: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF Lines 851-882 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=851&end_line=882 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout 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 def actual_advanced(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +cursor: Nat, -original: Core.Tensor, -before_source: Core.Tensor, -after_source: Core.Tensor, -before_target: Core.Tensor, -after_target: Core.Tensor, prefix: Transforms.Prefix, canonical: CanonicalStep) -> Transforms.Advanced: Transforms.Prefix{source_prior, words_prior, checked_prior, written_prior} = prefix CanonicalStep{converted, meaning} = canonical Transforms.Advanced{converted, step_source(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning), Equal.trans(Maybe<&2, F32>, Core.checked_observe(Layout.output(input, axes, plan), after_target, U32.from_nat(cursor)), Transforms.expected_output(input, axes, plan, before_source, U32.from_nat(cursor)), Transforms.expected_output(input, axes, plan, original, U32.from_nat(cursor)), step_value(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning), {\{ExpectedSame: equal => equal} : ExpectedSame -> {Transforms.expected_output(input, axes, plan, before_source, U32.from_nat(cursor)) == Transforms.expected_output(input, axes, plan, original, U32.from_nat(cursor)) : Maybe<&2, F32>}}( expected_same(input, axes, plan, original, before_source, U32.from_nat(cursor), source_prior))), step_route(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning), other => earlier => {\{PastFrame: checked => equal => checked} : PastFrame -> Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), after_target}, U32.from_nat(other))}( past_frame(Layout.output(input, axes, plan), before_target, after_target, cursor, other, converted, words_prior(other, earlier), checked_prior(other, earlier), earlier, step_frame(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning))), other => earlier => {\{PastFrame: checked => equal => equal} : PastFrame -> {Core.checked_observe(Layout.output(input, axes, plan), after_target, U32.from_nat(other)) == Core.checked_observe(Layout.output(input, axes, plan), before_target, U32.from_nat(other)) : Maybe<&2, F32>}}( past_frame(Layout.output(input, axes, plan), before_target, after_target, cursor, other, converted, words_prior(other, earlier), checked_prior(other, earlier), earlier, step_frame(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning)))} Uses (26): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 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=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat 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/tensor/core.bend&name=Dynamic https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=ObservationChecked 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/core.bend&name=checked_observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Plan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=output https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=CanonicalStep https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=ExpectedSame https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=PastFrame https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=expected_same https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=past_frame https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=step_frame https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=step_route https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=step_source https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=step_value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=Advanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=Prefix https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=expected_output