def CellIs

bendtorch-core@0.1.0.0 · src/tensor/parallel_proofs.bend:18

import Base

18# What cell `position` holds: the F32 its cell function computes from
19# `start`.
20def CellIs(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B),
21  +p: P, -start: (A & B), +count: Nat, +position: Nat, -observed: Maybe<&2, F32>) -> Type:
22  {observed == Some{Pair.fst(F32, (A & B), cell(p, position, start, Nat.is_lt(position, count)))} : Maybe<&2, F32>}