TensorChainPROOF.newer_chain: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend as TensorChainPROOF Lines 573-603 of bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&start_line=573&end_line=603 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend as Laws def newer_chain(newer: List<&1, Backward.Entry>, +node: Backward.Node, +shape: Shape.Shape, value: Core.Dynamic, saved: Backward.Saved, slot: Gradient.Slot, rest: List<&1, Backward.Entry>, +older: Nat, ones: Core.Tensor, made: {Core.new(shape, 1.0) == Done{ones} : Result<&2, &1, Core.Error, Core.Tensor>}) -> Passed rest), 1n+Nat.add(older, List.length(&1, Backward.Entry, newer)), older, Backward.at_head(1n+Nat.add(older, List.length(&1, Backward.Entry, newer)), older), Laws.seeds(List.length(&1, Backward.Entry, newer), shape, ones, older)>: match newer: case Nil{}: %add_zero(older) : Passed rest, 1n+_, older, Backward.at_head(1n+_, older), Laws.seeds(0n, shape, ones, older)> %eq_refl(older) : Passed rest, 1n+older, older, _, Laws.seeds(0n, shape, ones, older)> seeded_run(node, shape, value, saved, slot, rest, older, ones, made, started(Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), 1n+older)) case Con{Backward.Entry{+top, +top_shape, top_value, top_saved, top_slot}, tail}: %older_ne(older, List.length(&1, Backward.Entry, tail)) : Passed List.append(&1, Backward.Entry, tail, Backward.Entry{node, shape, value, saved, slot} <> rest), 1n+Nat.add(older, 1n+List.length(&1, Backward.Entry, tail)), older, _, Laws.seeds(1n+List.length(&1, Backward.Entry, tail), shape, ones, older)> %add_succ(older, List.length(&1, Backward.Entry, tail)) : Passed List.append(&1, Backward.Entry, tail, Backward.Entry{node, shape, value, saved, slot} <> rest), 1n+_, older, False{}, Laws.seeds(1n+List.length(&1, Backward.Entry, tail), shape, ones, older)> newer_step(top, top_shape, top_value, top_saved, top_slot, List.append(&1, Backward.Entry, tail, Backward.Entry{node, shape, value, saved, slot} <> rest), 1n+Nat.add(older, List.length(&1, Backward.Entry, tail)), older, Laws.seeds(List.length(&1, Backward.Entry, tail), shape, ones, older), newer_chain(tail, node, shape, value, saved, slot, rest, older, ones, made)) Uses (27): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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=List.length https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient.bend&name=Slot https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Entry https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Node https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Saved https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=at_head https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=unsets https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend&name=seeds https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=Passed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=add_succ https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=add_zero https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=eq_refl https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=newer_step https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=older_ne https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=seeded_run https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=started https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=new