def wired_entries

bendtorch-core@0.1.0.0 · src/autograd/backward_PROOF.bend:466

import Base
import bendtorch-core@0.1.0.0/src/autograd/backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend as Laws

466def wired_entries(+entries: List<&2, Backward.Entry>) ->
467  {Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)) == Laws.well_formed(Backward.nodes(entries)) : Bool}:
468  %Equal.sym(Nat, List.length(&2, Backward.Entry, entries), List.length(&2, Backward.Node, Backward.nodes(entries)), nodes_length(entries)) :
469    {Backward.wired(Backward.nodes(entries), _) == Laws.well_formed(Backward.nodes(entries)) : Bool}
470  Laws.wired_matches_operand_bounds(Backward.nodes(entries))