def prefix_written_case

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

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

306def prefix_written_case(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>,
307  -original: Core.Tensor<input>, -before: Core.Tensor<Layout.output(input, axes, plan)>, -after: Core.Tensor<Layout.output(input, axes, plan)>,
308  -cursor: Nat, +other: Nat,
309  prior: @+j: Nat -> @-earlier: {Nat.is_lt(j, cursor) == True{} : Bool} ->
310    {Core.checked_observe(Layout.output(input, axes, plan), before, U32.from_nat(j)) ==
311      Transforms.expected_output(input, axes, plan, original, U32.from_nat(j)) : Maybe<&2, F32>},
312  current: {Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(cursor)) ==
313    Transforms.expected_output(input, axes, plan, original, U32.from_nat(cursor)) : Maybe<&2, F32>},
314  frame: @+j: Nat -> @-earlier: {Nat.is_lt(j, cursor) == True{} : Bool} ->
315    {Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(j)) ==
316      Core.checked_observe(Layout.output(input, axes, plan), before, U32.from_nat(j)) : Maybe<&2, F32>},
317  split: Either<&2, &2, {Nat.is_lt(other, cursor) == True{} : Bool}, {other == cursor : Nat}>) ->
318  {Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(other)) ==
319    Transforms.expected_output(input, axes, plan, original, U32.from_nat(other)) : Maybe<&2, F32>}:
320  match split:
321    case Inl{+earlier}:
322      Equal.trans(Maybe<&2, F32>, Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(other)),
323        Core.checked_observe(Layout.output(input, axes, plan), before, U32.from_nat(other)),
324        Transforms.expected_output(input, axes, plan, original, U32.from_nat(other)), frame(other, earlier), prior(other, earlier))
325    case Inr{equal}:
326      %Equal.sym(Nat, other, cursor, equal) : {Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(_)) ==
327        Transforms.expected_output(input, axes, plan, original, U32.from_nat(_)) : Maybe<&2, F32>}
328      current