def right_pick

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

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

181def right_pick(-le: List<&2, Nat>, -re: List<&2, Nat>, -oe: List<&2, Nat>, +rows: List<&2, Shape.Row>,
182  +exact: {rows == Shape.index_table(le, re, oe) : List<&2, Shape.Row>},
183  same: Bool, +same_exact: {same == Elementwise.same_right(rows) : Bool},
184  zero: Bool, +zero_exact: {zero == Elementwise.zero_right(rows) : Bool}, +i: Nat) ->
185  {right_at(Elementwise.slot_of(same, zero), le, re, oe, Shape.Indexed{rows, exact}, i) == Shape.walk_right(rows, i) : Nat}:
186  match same zero:
187    case True{} zero:
188      Equal.sym(Nat, Shape.walk_right(rows, i), i, walk_right_same(rows, Equal.sym(Bool, True{}, Elementwise.same_right(rows), same_exact), i))
189    case False{} True{}:
190      Equal.sym(Nat, Shape.walk_right(rows, i), 0n, walk_right_zero(rows, Equal.sym(Bool, True{}, Elementwise.zero_right(rows), zero_exact), i))
191    case False{} False{}:
192      {==}