def Keeps

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

import Base

31# A cell hands its input state back unchanged.
32def Keeps(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B),
33  +p: P, -start: (A & B)) -> Type:
34  @+position: Nat -> @inside: Bool -> {Pair.snd(F32, (A & B), cell(p, position, start, inside)) == start : (A & B)}