PointwiseProof.expected_append: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof
Lines 34-41 of bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend&start_line=34&end_line=41

import Base
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws

def expected_append(+ops: List<&2, StorageLaws.Op>, +more: List<&2, StorageLaws.Op>, +n: Nat, +index: U32, +word: F32) ->
  {StorageLaws.expected(List.append(&2, StorageLaws.Op, ops, more), n, index, word) ==
    StorageLaws.expected(more, n, index, StorageLaws.expected(ops, n, index, word)) : F32}:
  match ops:
    case Nil{}:
      {==}
    case +op <> +rest:
      expected_append(rest, more, n, index, StorageLaws.latest(n, op, index, word))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=expected
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=latest