def naturals_append

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_PROOF.bend:655

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

655def naturals_append(+xs: List<&2, U32>, +ys: List<&2, U32>) ->
656  {Shape.naturals(List.append(&2, U32, xs, ys)) == List.append(&2, Nat, Shape.naturals(xs), Shape.naturals(ys)) : List<&2, Nat>}:
657  match xs:
658    case Nil{}:
659      {==}
660    case +head <> tail:
661      Equal.cong(List<&2, Nat>, List<&2, Nat>, rest => U32.to_nat(head) <> rest,
662        Shape.naturals(List.append(&2, U32, tail, ys)), List.append(&2, Nat, Shape.naturals(tail), Shape.naturals(ys)), naturals_append(tail, ys))