def fill_success
bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:603
import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
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/shape/nat_proofs.bend as Nats
603def fill_success(+values: List<&2, F32>, +shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat,
604 +room: Shape.LE(Nat.add(cursor, List.length(&2, F32, values)), Shape.elements(shape))) ->
605 FillSuccess<shape, Core.fill_values(values, shape, original, cursor)>:
606 match values:
607 case Nil{}:
608 FillSuccess{{==}}
609 case +value <> +rest:
610 fill_decided_success(shape, value, rest, cursor, U32.from_nat(cursor),
611 Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), original,
612 cursor_exact(shape, cursor, Nats.le_add_left(cursor, 1n+List.length(&2, F32, rest), Shape.elements(shape), room)),
613 cursor_inside(shape, cursor, U32.from_nat(cursor),
614 cursor_exact(shape, cursor, Nats.le_add_left(cursor, 1n+List.length(&2, F32, rest), Shape.elements(shape), room)),
615 cursor_below(cursor, List.length(&2, F32, rest), Shape.elements(shape), room)),
616 tensor => fill_success(rest, shape, tensor, 1n+cursor,
617 Nats.le_rewrite(Nat.add(1n+cursor, List.length(&2, F32, rest)), Nat.add(cursor, 1n+List.length(&2, F32, rest)),
618 Shape.elements(shape), add_successor(cursor, List.length(&2, F32, rest)), room)))