~/jendhub

def words_length

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:910

import bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend as ReduceReplayedProof
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 Laws

910def words_length(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat) ->
911  {List.length(&2, F32, Laws.words(shape, fill, ops, count)) == count : Nat}:
912  match count:
913    case 0n:
914      {==}
915    case 1n+previous:
916      +before = Laws.words(shape, fill, ops, previous)
917      Equal.trans(Nat, List.length(&2, F32, List.append(&2, F32, before, [Replayed.value(shape, fill, ops, U32.from_nat(previous))])),
918        1n+List.length(&2, F32, before), 1n+previous,
919        length_snoc(before, Replayed.value(shape, fill, ops, U32.from_nat(previous))),
920        Equal.cong(Nat, Nat, n => 1n+n, List.length(&2, F32, before), previous, words_length(shape, fill, ops, previous)))

Uses (13)

Used by (1)