def right_index

bendtorch-core@0.1.0.0 · src/tensor/elementwise_walk_proof.bend:202

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

202def right_index(-le: List<&2, Nat>, -re: List<&2, Nat>, -oe: List<&2, Nat>, +map: Shape.Index<le, re, oe>, +i: Nat) ->
203  {right_at(Elementwise.right_slot(le, re, oe, map), le, re, oe, map, i) == Elementwise.right_walk(le, re, oe, map, i) : Nat}:
204  match map:
205    case Shape.Indexed{+rows, +exact}:
206      right_pick(le, re, oe, rows, exact, Elementwise.same_right(rows), {==}, Elementwise.zero_right(rows), {==}, i)
207    case Shape.Unindexed{+zero}:
208      {==}