def natural_result_retains

bendtorch-core@0.1.0.0 · src/tensor/elementwise_PROOF.bend:336

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/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality

336def natural_result_retains(-shape: Shape.Shape, -cursor: Nat, -index: U32, -exact: {U32.to_nat(index) == cursor : Nat},
337  -left: Core.Dynamic, -right: Core.Dynamic, result: Elementwise.Step<shape>, -sources: StepSources<shape, left, right, result>) ->
338  NaturalSources<shape, cursor, left, right, Elementwise.natural_step_result(shape, cursor, index, exact, result)>:
339  match result:
340    case Elementwise.Stop{retained_left, retained_right, error}:
341      NaturalSources{
342        {\{StepSources: l => r => l} : StepSources<shape, left, right, Elementwise.Stop{retained_left, retained_right, error}> -> Totality.SameSource(left, retained_left)}(sources),
343        {\{StepSources: l => r => r} : StepSources<shape, left, right, Elementwise.Stop{retained_left, retained_right, error}> -> Totality.SameSource(right, retained_right)}(sources)}
344    case Elementwise.Continue{state}:
345      NaturalSources{
346        {\{StepSources: l => r => l} : StepSources<shape, left, right, Elementwise.Continue{state}> -> Totality.SameSource(left, step_left_owner(shape, Elementwise.Continue{state}))}(sources),
347        {\{StepSources: l => r => r} : StepSources<shape, left, right, Elementwise.Continue{state}> -> Totality.SameSource(right, step_right_owner(shape, Elementwise.Continue{state}))}(sources)}