def bound_at

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:435

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

435def bound_at(-rest: List<&2, Shape.Row>, -left: Nat, -stride: Nat, +by: BoundBy<rest, left, stride>, +q: Nat,
436  +below: {Nat.is_lt(q, stride) == True{} : Bool}) -> {Nat.is_lt(Shape.walk_left(rest, q), left) == True{} : Bool}:
437  BoundBy{+lt, +rt, +ot, +aligned, +rows, +size, +count} = by
438  %rows : {Nat.is_lt(Shape.walk_left(_, q), left) == True{} : Bool}
439  %size : {Nat.is_lt(Shape.walk_left(Shape.index_rows(lt, rt, ot), q), _) == True{} : Bool}
440  walk_left_below(lt, rt, ot, aligned, q,
441    %Equal.sym(Nat, Shape.numel(ot), stride, count) : {Nat.is_lt(q, _) == True{} : Bool}
442    below)