def rest_at

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

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

647# ... and so at every base.
648def rest_at(+rest: List<&2, Shape.Row>, +others: List<&2, Nat>, +inner: Nat, +stride: Nat, +walk: RestWalk(rest, others, inner, stride),
649  +base: Nat) ->
650  {masked(stride, rest, inner, base, 0n) ==
651    visited(rest, others, Reduce.first_span(rest, others), inner, base, Reduce.first_digit(rest, inner)) : List<&2, Nat>}:
652  %Equal.sym(List<&2, Nat>, masked(stride, rest, inner, base, 0n), shift(base, masked(stride, rest, inner, 0n, 0n)),
653    masked_base(stride, rest, inner, base, 0n)) :
654    {_ == visited(rest, others, Reduce.first_span(rest, others), inner, base, Reduce.first_digit(rest, inner)) : List<&2, Nat>}
655  %Equal.sym(List<&2, Nat>, visited(rest, others, Reduce.first_span(rest, others), inner, base, Reduce.first_digit(rest, inner)),
656    shift(base, visited(rest, others, Reduce.first_span(rest, others), inner, 0n, Reduce.first_digit(rest, inner))),
657    visited_base(rest, others, Reduce.first_span(rest, others), inner, base, Reduce.first_digit(rest, inner))) :
658    {shift(base, masked(stride, rest, inner, 0n, 0n)) == _ : List<&2, Nat>}
659  Equal.cong(List<&2, Nat>, List<&2, Nat>, xs => shift(base, xs), masked(stride, rest, inner, 0n, 0n),
660    visited(rest, others, Reduce.first_span(rest, others), inner, 0n, Reduce.first_digit(rest, inner)), walk)