def kept_below

bendtorch-core@0.1.0.0 · src/autograd/reduce_parallel_proof.bend:198

import Base
import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as Fiber

198def kept_below(+keep: Bool, +position: Nat, +rest: List<&2, Nat>, +bound: Nat,
199  +inside: {Nat.is_lt(position, bound) == True{} : Bool}, +others: {all_below(rest, bound) == True{} : Bool}) ->
200  {all_below(Fiber.kept(keep, position, rest), bound) == True{} : Bool}:
201  match keep:
202    case True{}:
203      %Equal.sym(Bool, Nat.is_lt(position, bound), True{}, inside) : {Bool.and(_, all_below(rest, bound)) == True{} : Bool}
204      others
205    case False{}:
206      others