def left_index

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

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

194def left_index(-le: List<&2, Nat>, -re: List<&2, Nat>, -oe: List<&2, Nat>, +map: Shape.Index<le, re, oe>, +i: Nat) ->
195  {left_at(Elementwise.left_slot(le, re, oe, map), le, re, oe, map, i) == Elementwise.left_walk(le, re, oe, map, i) : Nat}:
196  match map:
197    case Shape.Indexed{+rows, +exact}:
198      left_pick(le, re, oe, rows, exact, Elementwise.same_left(rows), {==}, Elementwise.zero_left(rows), {==}, i)
199    case Shape.Unindexed{+zero}:
200      {==}