def words_snoc
bendtorch-core@0.1.0.0 · src/tensor/contracts/binary_proofs.bend:302
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend as BinaryProofs
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts
302def words_snoc(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +previous: Nat, +word: F32, +other: F32,
303 +before: List<&2, F32>, rest: {Contracts.words(shape, fill, ops, previous) == before : List<&2, F32>}, last: {word == other : F32}) ->
304 {List.append(&2, F32, Contracts.words(shape, fill, ops, previous), [word]) == List.append(&2, F32, before, [other]) : List<&2, F32>}:
305 Equal.trans(List<&2, F32>, List.append(&2, F32, Contracts.words(shape, fill, ops, previous), [word]),
306 List.append(&2, F32, before, [word]), List.append(&2, F32, before, [other]),
307 Equal.cong(List<&2, F32>, List<&2, F32>, values => List.append(&2, F32, values, [word]), Contracts.words(shape, fill, ops, previous), before, rest),
308 Equal.cong(F32, List<&2, F32>, value => List.append(&2, F32, before, [value]), word, other, last))