def matrix_part

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend as Batched
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend as Laws

680def matrix_part(+rows: U32, +lv: Bool, +columns: U32, +rv: Bool) ->
681  {Shape.naturals(Batched.matrix_dims(rows, lv, columns, rv)) ==
682    List.append(&2, Nat, Laws.kept(lv, U32.to_nat(rows)), Laws.kept(rv, U32.to_nat(columns))) : List<&2, Nat>}:
683  match lv rv:
684    case True{} True{}:
685      {==}
686    case True{} False{}:
687      {==}
688    case False{} True{}:
689      {==}
690    case False{} False{}:
691      {==}