~/jendhub

def words_length

bendtorch-core@0.1.0.0 · src/autograd/reduce_fold_PROOF.bend:66

import bendtorch-core@0.1.0.0/src/autograd/reduce_fold_PROOF.bend as ReduceFoldPROOF
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/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts

66def words_length(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat) ->
67  {List.length(&2, F32, Contracts.words(shape, fill, ops, count)) == count : Nat}:
68  match count:
69    case 0n:
70      {==}
71    case 1n+previous:
72      +before = Contracts.words(shape, fill, ops, previous)
73      Equal.trans(Nat, List.length(&2, F32, List.append(&2, F32, before, [Replayed.value(shape, fill, ops, U32.from_nat(previous))])),
74        1n+List.length(&2, F32, before), 1n+previous,
75        length_snoc(before, Replayed.value(shape, fill, ops, U32.from_nat(previous))),
76        Equal.cong(Nat, Nat, n => 1n+n, List.length(&2, F32, before), previous, words_length(shape, fill, ops, previous)))

Uses (13)

Used by (1)