def words_snoc
bendtorch-core@0.1.0.0 · src/tensor/permute_values.bend:65
import bendtorch-core@0.1.0.0/src/tensor/permute_values.bend as PermuteValues
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
65def words_snoc(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +previous: Nat, +word: F32, +other: F32,
66 +before: List<&2, F32>, rest: {Contracts.words(shape, fill, ops, previous) == before : List<&2, F32>}, last: {word == other : F32}) ->
67 {List.append(&2, F32, Contracts.words(shape, fill, ops, previous), [word]) == List.append(&2, F32, before, [other]) : List<&2, F32>}:
68 Equal.trans(List<&2, F32>, List.append(&2, F32, Contracts.words(shape, fill, ops, previous), [word]),
69 List.append(&2, F32, before, [word]), List.append(&2, F32, before, [other]),
70 Equal.cong(List<&2, F32>, List<&2, F32>, values => List.append(&2, F32, values, [word]), Contracts.words(shape, fill, ops, previous), before, rest),
71 Equal.cong(F32, List<&2, F32>, value => List.append(&2, F32, before, [value]), word, other, last))