def pair_certified

bendtorch-core@0.1.0.0 · src/tensor/parallel.bend:126

import Base

126def pair_certified(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> A & B -> Bool -> F32 & (A & B),
127  +p: P, +count: Nat, +base: Nat, low: F32 & (A & B)) -> Certified<(A & B), 1n, pair(~P, ~A, ~B, ~cell, p, count, base, low)>:
128  (x, state) = low
129  (l, r) = state
130  pair_joined(~(A & B), x, cell(p, Nat.add(1n, base), (l, r), Nat.is_lt(Nat.add(1n, base), count)))