def passed_chain
bendtorch-core@0.1.0.0 · src/autograd/tensor_chain_PROOF.bend:605
import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend as TensorChainPROOF
import Base
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
605def passed_chain(-entries: List<&1, Backward.Entry>, -count: Nat, -output: Nat, -selected: Bool, -slots: List<&1, Gradient.Slot>,
606 -gradients: List<&1, Gradient.Slot>,
607 succeeded: {Laws.result(Backward.pass(entries, count, output, selected)) == Done{gradients} : Laws.Slots()},
608 out: Passed<entries, count, output, selected, slots>) -> {Laws.chained(entries, slots, count, Nil{}) == Done{gradients} : Laws.Slots()}:
609 match out:
610 case PassKept{done, found, passed, chained}:
611 Equal.trans(Laws.Slots(), Laws.chained(entries, slots, count, Nil{}), Done{found}, Done{gradients}, chained,
612 Equal.trans(Laws.Slots(), Done{found}, Laws.result(Backward.pass(entries, count, output, selected)), Done{gradients},
613 Equal.sym(Laws.Slots(), Laws.result(Backward.pass(entries, count, output, selected)), Done{found},
614 Equal.cong(Backward.Swept(), Laws.Slots(), pair => Laws.result(pair), Backward.pass(entries, count, output, selected),
615 (done, Done{found}), passed)),
616 succeeded))
617 case PassStopped{done, error, passed}:
618 Empty.absurd({Laws.chained(entries, slots, count, Nil{}) == Done{gradients} : Laws.Slots()},
619 done_fail(error, gradients,
620 Equal.trans(Laws.Slots(), Fail{error}, Laws.result(Backward.pass(entries, count, output, selected)), Done{gradients},
621 Equal.sym(Laws.Slots(), Laws.result(Backward.pass(entries, count, output, selected)), Fail{error},
622 Equal.cong(Backward.Swept(), Laws.Slots(), pair => Laws.result(pair), Backward.pass(entries, count, output, selected),
623 (done, Fail{error}), passed)),
624 succeeded)))