ParallelProofs.Keeps: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as ParallelProofs Lines 31-34 of bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&start_line=31&end_line=34 import Base # A cell hands its input state back unchanged. def Keeps(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B), +p: P, -start: (A & B)) -> Type: @+position: Nat -> @inside: Bool -> {Pair.snd(F32, (A & B), cell(p, position, start, inside)) == start : (A & B)} Uses (5): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd